theorem :: MATRIXR2:11

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