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

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

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

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

assume not k + 1 is trivial ; :: thesis: S₁[k + 1]

per cases ( k = 1 or k <> 1 ) ;

suppose k = 1 ; :: thesis: S₁[k + 1]

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

end;

suppose k <> 1 ; :: thesis: S₁[k + 1]

then not k is trivial ;
hence S₁[k + 1] by A2, A4; :: thesis: verum

end;

end;

end;

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

end;

A5: S₁[1] by Def1;
for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A5, A3);
hence for k being non trivial Nat holds P₁[k] ; :: thesis: verum