let R be non empty Abelian addLoopStr ; :: thesis: for a being Element of R
for n being Element of NAT holds n * a = a * n
let a be Element of R; :: thesis: for n being Element of NAT holds n * a = a * n
let n be Element of NAT ; :: thesis: n * a = a * n
defpred S₁[ Nat] means $1 * a = a * $1;

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

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
assume S₁[k] ; :: thesis: S₁[k + 1]
then (kk + 1) * a = a + (a * k) by Def3
.= a * (kk + 1) by Def4 ;
hence S₁[k + 1] ; :: thesis: verum

end;

0 * a = 0. R by Def3
.= a * 0 by Def4 ;
then A2: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A1);
hence n * a = a * n ; :: thesis: verum