let R be non empty left_zeroed add-associative addLoopStr ; :: thesis: for a being Element of R
for n, m being Nat holds (n + m) * a = (n * a) + (m * a)
let a be Element of R; :: thesis: for n, m being Nat holds (n + m) * a = (n * a) + (m * a)
let n, m be Nat; :: thesis: (n + m) * a = (n * a) + (m * a)
defpred S₁[ Nat] means ($1 + m) * a = ($1 * a) + (m * a);

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]
((k + 1) + m) * a = ((k + m) + 1) * a
.= a + ((k + m) * a) by Def3
.= a + ((kk * a) + (m * a)) by A2
.= (a + (k * a)) + (m * a) by RLVECT_1:def 3
.= ((kk + 1) * a) + (m * a) by Def3 ;
hence S₁[k + 1] ; :: thesis: verum

end;

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