defpred S₁[ Nat] means ( not $1 is zero implies P₁[$1] );

A3: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: ( not k + 1 is zero implies S₁[k + 1] )

assume not k + 1 is zero ; :: thesis: S₁[k + 1]
( k = 0 or not k is zero ) ;
hence S₁[k + 1] by A1, A2, A4; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A5: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A3);
hence for k being non zero Nat holds P₁[k] ; :: thesis: verum