theorem :: MATRIXR2:13

for a, b being Real
for A being Matrix of REAL holds (a - b) * A = (a * A) - (b * A)