let R be non empty add-associative right_zeroed addLoopStr ; :: thesis: for a being Element of R
for n, m being Element of NAT holds a * (n + m) = (a * n) + (a * m)
let a be Element of R; :: thesis: for n, m being Element of NAT holds a * (n + m) = (a * n) + (a * m)
let n, m be Element of NAT ; :: thesis: a * (n + m) = (a * n) + (a * m)
defpred S₁[ Nat] means a * (n + $1) = (a * n) + (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] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
a * (n + (k + 1)) = a * ((n + kk) + 1)
.= ((a * n) + (a * kk)) + a by A2, Def4
.= (a * n) + ((a * k) + a) by RLVECT_1:def 3
.= (a * n) + (a * (kk + 1)) by Def4 ;
hence S₁[k + 1] ; :: thesis: verum

end;

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