now :: thesis: ex k being Nat st P₁[k]

deffunc H₁( Nat) -> Element of NAT = In (F₁($1),NAT);
consider f being sequence of NAT such that
A2: for k being Element of NAT holds f . k = H₁(k) from FUNCT_2:sch 4();
A3: f . 0 in rng f by FUNCT_2:4;
rng f c= NAT

proof

let x be object ; :: 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 object 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 = H₁(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 object 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 = H₁(x) & f . (x + 1) = H₁(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] & ( for n being Nat st P₁[n] holds
k <= n ) ) from NAT_1:sch 5(A9);
take k ; :: thesis: ( P₁[k] & ( for n being Nat st P₁[n] holds
k <= n ) )
thus ( P₁[k] & ( for n being Nat st P₁[n] holds
k <= n ) ) by A10; :: thesis: verum