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 natural number holds f . n = H₁(f | n) from ALGSTR_4:sch 2();
for y being set st y in rng f holds
y in F₁()

proof

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

end;

then rng f c= F₁() by TARSKI:def 3;
then reconsider f9 = f as Function of NAT,F₁() by A1, FUNCT_2:2;
take f9 ; :: thesis: for n being natural number holds f9 . n = F₂((f9 | n))
let n be natural number ; :: 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