let R be non empty left_zeroed add-associative right_zeroed 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₁[ Element of NAT ] means $1 * a = a * $1;

A1: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
(k + 1) * a = (k * a) + (1 * a) by Th16
.= (k * a) + a by Th14
.= (a * k) + (a * 1) by A2, Th15
.= a * (k + 1) by Th17 ;
hence S₁[k + 1] ; :: thesis: verum

end;

0 * a = 0. R by Def6
.= a * 0 by Def7 ;
then A3: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A1);
hence n * a = a * n ; :: thesis: verum