let R be non empty right_add-cancelable left_zeroed distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for a, b being Element of R
for n being Element of NAT holds b * (n * a) = (b * a) * n
let a, b be Element of R; :: thesis: for n being Element of NAT holds b * (n * a) = (b * a) * n
let n be Element of NAT ; :: thesis: b * (n * a) = (b * a) * n
defpred S₁[ Nat] means b * ($1 * a) = (b * 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 A2: S₁[k] ; :: thesis: S₁[k + 1]
b * ((kk + 1) * a) = b * (a + (k * a)) by Def3
.= (b * a) + ((b * a) * k) by A2, VECTSP_1:def 2
.= ((b * a) * 1) + ((b * a) * k) by Th14
.= (b * a) * (kk + 1) by Th16 ;
hence S₁[k + 1] ; :: thesis: verum

end;

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