theorem Th51: :: BKMODEL1:59

for n being Nat
for a being Real
for M being Matrix of n,REAL
for x being FinSequence of REAL st n > 0 & len x = n holds
a * (M * x) = (a * M) * x