let x be FinSequence of REAL ; :: thesis: for A, B being Matrix of REAL st len x = len A & width A = len B holds
x * (A * B) = (x * A) * B
let A, B be Matrix of REAL; :: thesis: ( len x = len A & width A = len B implies x * (A * B) = (x * A) * B )
assume that
A1: len x = len A and
A2: width A = len B ; :: thesis: x * (A * B) = (x * A) * B
width (LineVec2Mx x) = len x by MATRIXR1:def 10;
hence x * (A * B) = Line ((((LineVec2Mx x) * A) * B),1) by A1, A2, MATRIX_3:33
.= (x * A) * B by A1, Th56 ;
:: thesis: verum