deffunc H₁( set ) -> Element of F₁() = F₂((IFXFinSequence ($1,F₁())));
consider f being Function such that
A1: dom f = NAT and
A2: for n being Nat holds f . n = H₁(f | n) from ALGSTR_4:sch 2();
for y being object st y in rng f holds
y in F₁()

proof

let y be object ; :: thesis: ( y in rng f implies y in F₁() )
assume y in rng f ; :: thesis: y in F₁()
then consider x being object such that
A3: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
reconsider x = x as Nat by A1, A3;
y = F₂((IFXFinSequence ((f | x),F₁()))) by A3, A2;
hence y in F₁() ; :: thesis: verum

end;

then rng f c= F₁() ;
then reconsider f9 = f as sequence of F₁() by A1, FUNCT_2:2;
take f9 ; :: thesis: for n being Nat holds f9 . n = F₂((f9 | n))
let n be Nat; :: thesis: f9 . n = F₂((f9 | n))
f . n = F₂((IFXFinSequence ((f9 | n),F₁()))) by A2
.= F₂((f9 | n)) by Def1 ;
hence f9 . n = F₂((f9 | n)) ; :: thesis: verum