Theorem fn_unique_value

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.
05. 1 ⊢ ∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, conj_elimr 3.
06. 1 ⊢ ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_elim 5.
07. 1 ⊢ ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_elim 6.
08. 1 ⊢ (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2, uq_elim 7.
fn_unique_value. ⊢ function f → (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2,
  subj_intro 8.