let a be Real; :: thesis: for x being FinSequence of REAL
for A being Matrix of REAL st width A = len x & len x > 0 & len A > 0 holds
A * (a * x) = a * (A * x)
let x be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st width A = len x & len x > 0 & len A > 0 holds
A * (a * x) = a * (A * x)
let A be Matrix of REAL ; :: thesis: ( width A = len x & len x > 0 & len A > 0 implies A * (a * x) = a * (A * x) )
assume A1: ( width A = len x & len x > 0 & len A > 0 ) ; :: thesis: A * (a * x) = a * (A * x)
then A2: len (ColVec2Mx x) = len x by MATRIXR1:def 9;
width (ColVec2Mx x) = 1 by A1, MATRIXR1:def 9;
then A3: 1 <= width (A * (ColVec2Mx x)) by A1, A2, MATRIX_3:def 4;
thus A * (a * x) = Col (A * (a * (ColVec2Mx x))),1 by A1, MATRIXR1:47
.= Col (a * (A * (ColVec2Mx x))),1 by A1, A2, MATRIXR1:40
.= a * (A * x) by A3, MATRIXR1:56 ; :: thesis: verum