consider t being non zero Nat such that
A3: P₁[t] by A1;
defpred S₁[ Nat] means P₁[$1 + 1];

A4: now :: thesis: for k being Nat st k <> 0 & S₁[k] holds
ex l being Nat st
( l < k & S₁[l] )

let k be Nat; :: thesis: ( k <> 0 & S₁[k] implies ex l being Nat st
( l < k & S₁[l] ) )
assume that
A5: k <> 0 and
A6: S₁[k] ; :: thesis: ex l being Nat st
( l < k & S₁[l] )
reconsider k1 = k + 1 as non zero Element of NAT ;
k + 1 > 0 + 1 by A5, XREAL_1:6;
then consider n being non zero Nat such that
A7: n < k1 and
A8: P₁[n] by A2, A6;
consider l being Nat such that
A9: n = l + 1 by NAT_1:6;
take l = l; :: thesis: ( l < k & S₁[l] )
thus l < k by A7, A9, XREAL_1:6; :: thesis: S₁[l]
thus S₁[l] by A8, A9; :: thesis: verum

end;

ex s being Nat st t = s + 1 by NAT_1:6;
then A10: ex k being Nat st S₁[k] by A3;
S₁[ 0 ] from NAT_1:sch 7(A10, A4);
hence P₁[1] ; :: thesis: verum