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 that
A1: len x = width B and
A2: width A = len B and
A3: len x > 0 and
A4: len B > 0 ; :: thesis: (A * B) * x = A * (B * x)
len (ColVec2Mx x) = len x by A3, MATRIXR1:def 9;
hence (A * B) * x = Col ((A * (B * (ColVec2Mx x))),1) by A1, A2, MATRIX_3:33
.= A * (B * x) by A1, A3, A4, Th58 ;
:: thesis: verum