Sets of ordered pairs

Def: Let w be a set of ordered pairs. The inverse of w is defined by:
w-1 = { (y,x) | (x,y)∈w }

Def: Let w be a set of ordered pairs and p be any set. The restriction of w on p is defined by:
restrict(w,p) = { (x,y)∈w | x∈p }

Def: Let f and g be sets of ordered pairs. The composition f∘g is defined by:
f∘g = { (x,z) | (x,y)∈g ∧ (y,z)∈f }

Def: Let w be a set of ordered pairs. The domain and image of w are defined by:
dom(w) = { x | (x,y) ∈ w }
image(w) = { y | (x,y) ∈ w }

Note:
dom(∅) = ∅
image(∅) = ∅
∀w, dom(w-1) = image(w)
∀w, image(w-1) = dom(w)
∀w, restrict(w,∅) = ∅
∀p, restrict(∅,p) = ∅
∀w,p, dom(restrict(w,p)) = dom(w)∩p
∀w, w∘∅ = ∅
∀w, ∅∘w = ∅