consider f being Function such that
A1: dom f = NAT and
A2: f . 0 = F₂() and
A3: for n being Nat holds f . (n + 1) = F₃(n,(f . n)) from NAT_1:sch 11();
for x being object st x in NAT holds
f . x in F₁()

proof

let x be object ; :: thesis: ( x in NAT implies f . x in F₁() )
assume x in NAT ; :: thesis: f . x in F₁()
then reconsider n = x as Nat ;

per cases ( n = 0 or ex k being Nat st n = k + 1 ) by Th6;

suppose n = 0 ; :: thesis: f . x in F₁()

hence f . x in F₁() by A2; :: thesis: verum

end;

suppose ex k being Nat st n = k + 1 ; :: thesis: f . x in F₁()

then consider k being Nat such that
A4: n = k + 1 ;
f . n = F₃(k,(f . k)) by A3, A4;
hence f . x in F₁() ; :: thesis: verum

end;

end;

end;

then reconsider f = f as sequence of F₁() by A1, FUNCT_2:3;
take f ; :: thesis: ( f . 0 = F₂() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) )
thus ( f . 0 = F₂() & ( for n being Nat holds f . (n + 1) = F₃(n,(f . n)) ) ) by A2, A3; :: thesis: verum