theorem :: MATRIXR2:53

for a being Real
for x being FinSequence of REAL
for A being Matrix of REAL st width A = len x & len x > 0 holds
A * (a * x) = a * (A * x)