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
M * (a * x) = (a * M) * x