now

assume A2: for k being Element of NAT holds P₁[k] ; :: thesis: contradiction
consider f being Function of NAT , NAT such that
A3: 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 RELSET_1:12;
set m = min rf;
min rf in rf by XXREAL_2:def 7;
then consider x being set such that
A4: ( x in dom f & min rf = f . x ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A4, FUNCT_2:def 1;
( f . x = F₁(x) & f . (x + 1) = F₁((x + 1)) ) by A3;
then A5: ( f . (x + 1) < f . x or P₁[x] ) by A1;
f . (x + 1) in rf by FUNCT_2:6;
hence contradiction by A2, A4, A5, XXREAL_2:def 7; :: thesis: verum

end;

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