let R be non empty left_zeroed add-associative addLoopStr ; :: thesis: for a being Element of R
for n, m being Element of NAT holds (n + m) * a = (n * a) + (m * a)
let a be Element of R; :: thesis: for n, m being Element of NAT holds (n + m) * a = (n * a) + (m * a)
let n, m be Element of NAT ; :: thesis: (n + m) * a = (n * a) + (m * a)
defpred S₁[ Element of NAT ] means ($1 + m) * a = ($1 * a) + (m * a);
(0 + m) * a = (0. R) + (m * a) by ALGSTR_1:def 5
.= (0 * a) + (m * a) by Def6 ;
then A1: S₁[ 0 ] ;

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
((k + 1) + m) * a = ((k + m) + 1) * a
.= a + ((k * a) + (m * a)) by A3, Def6
.= (a + (k * a)) + (m * a) by RLVECT_1:def 6
.= ((k + 1) * a) + (m * a) by Def6 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence (n + m) * a = (n * a) + (m * a) ; :: thesis: verum