Proof 01. 1 ⊢ function f, hypo. 02. ⊢ function f → relation f ∧ ∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, bij_eliml function_equi. 03. 1 ⊢ relation f ∧ ∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, subj_elim 2 1. 04. 1 ⊢ relation f, conj_eliml 3. fn_is_rel. ⊢ function f → relation f, subj_intro 4.