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