The restriction of a function f to A, written f|A in common notation, is the truncation of it to the product A × UnivCl. The domain of f|A is (dom f) ∩ A, as shown in dom_restr. Thus, in a situation with A ⊆ dom f, the domain of f|A is simply A.