let x be FinSequence of REAL ; :: thesis: for A, B being Matrix of REAL st len x = width B & width A = len B & len x > 0 & len B > 0 holds
(A * B) * x = A * (B * x)
let A, B be Matrix of REAL ; :: thesis: ( len x = width B & width A = len B & len x > 0 & len B > 0 implies (A * B) * x = A * (B * x) )
assume A1: ( len x = width B & width A = len B & len x > 0 & len B > 0 ) ; :: thesis: (A * B) * x = A * (B * x)
then len (ColVec2Mx x) = len x by MATRIXR1:def 9;
hence (A * B) * x = Col (A * (B * (ColVec2Mx x))),1 by A1, MATRIX_3:35
.= A * (B * x) by A1, Th58 ;
:: thesis: verum