theorem Lm11: :: E_TRANS1:1

for R being domRing
for n, m being Nat
for b being Element of R holds (n * m) * b = n * (m * b)