let k be non zero Element of NAT ; :: thesis: P₁[k]
defpred S₁[ Nat] means ex m being non zero Element of NAT st
( m = $1 & P₁[m] );

A2: now :: thesis: for k being Nat st k >= 1 & ( for n being Nat st n >= 1 & n < k holds
S₁[n] ) holds
S₁[k]

let k be Nat; :: thesis: ( k >= 1 & ( for n being Nat st n >= 1 & n < k holds
S₁[n] ) implies S₁[k] )
assume that
A3: k >= 1 and
A4: for n being Nat st n >= 1 & n < k holds
S₁[n] ; :: thesis: S₁[k]
reconsider m = k as non zero Element of NAT by A3, ORDINAL1:def 12;

now :: thesis: for n being non zero Element of NAT st n < m holds
P₁[n]

let n be non zero Element of NAT ; :: thesis: ( n < m implies P₁[n] )
assume A5: n < m ; :: thesis: P₁[n]
n >= 1 by Lm1;
then S₁[n] by A4, A5;
hence P₁[n] ; :: thesis: verum

end;

then P₁[m] by A1;
hence S₁[k] ; :: thesis: verum

end;

A6: for k being Nat st k >= 1 holds
S₁[k] from NAT_1:sch 9(A2);
k >= 1 by Lm1;
then ex m being non zero Element of NAT st
( m = k & P₁[m] ) by A6;
hence P₁[k] ; :: thesis: verum