Proof function_unfold. ⊢ function f → relation f ∧ (∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2), bij_eliml function_equi.