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

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

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

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

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

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

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

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

.= F_{2}(a)
by FINSEQ_1:40
; :: thesis: verum

consider f being Function of (1 -tuples_on F

A1: for a being Element of 1 -tuples_on F

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

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

let a be Element of F

reconsider p = <*a*> as Element of 1 -tuples_on F

thus f . <*a*> = H

.= F