theorem Th47: :: BKMODEL1:55

for n being Nat
for a being Element of F_Real
for A, B being Matrix of n,F_Real st n > 0 holds
(a * A) * B = a * (A * B)