deffunc H_{1}( Element of 2 -tuples_on F_{1}()) -> Element of F_{1}() = F_{2}(($1 . 1),($1 . 2));

consider f being Function of (2 -tuples_on F_{1}()),F_{1}() such that

A1: for a being Element of 2 -tuples_on F_{1}() holds f . a = H_{1}(a)
from FUNCT_2:sch 4();

reconsider f = f as non empty homogeneous quasi_total 2 -ary PartFunc of (F_{1}() *),F_{1}() by Th44;

take f ; :: thesis: for a, b being Element of F_{1}() holds f . <*a,b*> = F_{2}(a,b)

let a, b be Element of F_{1}(); :: thesis: f . <*a,b*> = F_{2}(a,b)

reconsider p = <*a,b*> as Element of 2 -tuples_on F_{1}() by FINSEQ_2:101;

thus f . <*a,b*> = H_{1}(p)
by A1

.= F_{2}(a,(p . 2))
by FINSEQ_1:44

.= F_{2}(a,b)
by FINSEQ_1:44
; :: thesis: verum

consider f being Function of (2 -tuples_on F

A1: for a being Element of 2 -tuples_on F

reconsider f = f as non empty homogeneous quasi_total 2 -ary PartFunc of (F

take f ; :: thesis: for a, b being Element of F

let a, b be Element of F

reconsider p = <*a,b*> as Element of 2 -tuples_on F

thus f . <*a,b*> = H

.= F

.= F