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:
assume x in NAT ; :: thesis:
then reconsider n = x as Nat ;

per cases by Th6;

suppose n = 0 ; :: thesis:

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

end;

suppose ex k being Nat st n = k + 1 ; :: thesis:

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:

end;

end;

end;

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