now

consider f being Function of NAT ,NAT such that
A2: for k being Element of NAT holds f . k = F₁(k) from FUNCT_2:sch 4();
A: f . 0 in rng f by FUNCT_2:6;
rng f c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in NAT )
assume x in rng f ; :: thesis: x in NAT
then consider y being set such that
B: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
reconsider y1 = y as Element of NAT by B, FUNCT_2:def 1;
x = F₁(y1) by B, A2;
hence x in NAT ; :: thesis: verum

end;

then reconsider rf = rng f as non empty Subset of NAT by A;
set m = min* rf;
min* rf in rf by MinS;
then consider x being set such that
A3: x in dom f and
A4: min* rf = f . x by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A3, FUNCT_2:def 1;
( f . x = F₁(x) & f . (x + 1) = F₁((x + 1)) ) by A2;
then A5: ( f . (x + 1) < f . x or P₁[x] ) by A1;
assume A6: for k being Nat holds P₁[k] ; :: thesis: contradiction
f . (x + 1) in rf by FUNCT_2:6;
hence contradiction by MinS, A6, A4, A5; :: thesis: verum

end;

then A7: ex k being Nat st P₁[k] ;
consider k being Nat such that
A8: P₁[k] and
A9: for n being Nat st P₁[n] holds
k <= n from NAT_1:sch 5(A7);
( k in NAT & ( for n being Element of NAT st P₁[n] holds
k <= n ) ) by A9, ORDINAL1:def 13;
hence ex k being Element of NAT st
( P₁[k] & ( for n being Element of NAT st P₁[n] holds
k <= n ) ) by A8; :: thesis: verum