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();
A3: f . 0 in rng f by FUNCT_2:4;
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
A4: ( y in dom f & x = f . y ) by FUNCT_1:def 3;
reconsider y1 = y as Element of NAT by A4, FUNCT_2:def 1;
x = F₁(y1) by A4, A2;
hence x in NAT ; :: thesis: verum

end;

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

end;

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