A0: k is Nat by TARSKI:1;
defpred S₁[ Nat] means n * n is natural ;
A1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume S₁[m] ; :: thesis: S₁[m + 1]
then reconsider k = n * m as Nat ;
k + n is Nat ;
hence S₁[m + 1] ; :: thesis: verum

end;

A2: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A2, A1);
hence n * k is natural by A0; :: thesis: verum