theorem Th29: :: MATGRP_0:20
for R being Ring
for n, k, m being Nat st ( k = 0 implies m = 0 ) holds
for r being Element of R
for A being Matrix of k,m,R
for B being Matrix of m,n,R holds (r * A) * B = r * (A * B)