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();
f . 0 in rng f by FUNCT_2:6;
then reconsider rf = rng f as non empty Subset of NAT by RELAT_1:def 19;
set m = min rf;
min rf in rf by XXREAL_2:def 7;
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 Element of NAT holds P₁[k] ; :: thesis: contradiction
f . (x + 1) in rf by FUNCT_2:6;
hence contradiction by A6, A4, A5, XXREAL_2:def 7; :: 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