theorem :: MATRIXR2:17
for A, B, C being Matrix of REAL st len A = len B & width A = width B & len C = width A & len A > 0 & len C > 0 holds
(A - B) * C = (A * C) - (B * C) by Th16;