theorem Th15: :: BINOM:15

for R being non empty left_zeroed add-associative addLoopStr
for a being Element of R
for n, m being Nat holds (n + m) * a = (n * a) + (m * a)