Theorem function_intro

Proof
01. 1 ⊢ relation f, hypo.
02. 2 ⊢ ∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, hypo.
03. 1, 2 ⊢ relation f ∧
  ∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, conj_intro 1 2.
04. ⊢ relation f ∧
  (∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2) →
  function f, bij_elimr function_equi.
05. 1, 2 ⊢ function f, subj_elim 4 3.
function_intro. ⊢ relation f →
  (∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2) →
  function f, subj_intro_ii 5.