Proposition 1.5.31.  Let X, Y be sets, f : X ↔ Y be a bijection, y ∈ Y. Then:
f(f-1(y)) = y
Proof.
f ∘ f-1 = idY by definition of f-1 ⇒def ∀ z ∈ Y : f(f-1(z)) = z ⇒y ∈ Y f(f-1(y)) = y