deffunc H₁( Element of 2 -tuples_on F₁()) -> Element of F₁() = F₂(($1 . 1),($1 . 2));
consider f being Function of (2 -tuples_on F₁()),F₁() such that
A1: for a being Element of 2 -tuples_on F₁() holds f . a = H₁(a) from FUNCT_2:sch 4();
reconsider f = f as non empty homogeneous quasi_total 2 -ary PartFunc of (F₁() *),F₁() by Th44;
take f ; :: thesis: for a, b being Element of F₁() holds f . <*a,b*> = F₂(a,b)
let a, b be Element of F₁(); :: thesis: f . <*a,b*> = F₂(a,b)
reconsider p = <*a,b*> as Element of 2 -tuples_on F₁() by FINSEQ_2:101;
thus f . <*a,b*> = H₁(p) by A1
.= F₂(a,(p . 2))
.= F₂(a,b) ; :: thesis: verum