let x be FinSequence of REAL ; :: thesis: for A, B being Matrix of REAL st len A = len B & width A = width B & width A = len x & len x > 0 holds
(A + B) * x = (A * x) + (B * x)
let A, B be Matrix of REAL; :: thesis: ( len A = len B & width A = width B & width A = len x & len x > 0 implies (A + B) * x = (A * x) + (B * x) )
assume that
A1: ( len A = len B & width A = width B ) and
A2: width A = len x and
A4: len x > 0 ; :: thesis: (A + B) * x = (A * x) + (B * x)
A5: len (ColVec2Mx x) = len x by A4, Def9;
then A6: len (A * (ColVec2Mx x)) = len A by A2, MATRIX_3:def 4
.= len (B * (ColVec2Mx x)) by A1, A2, A5, MATRIX_3:def 4 ;
A7: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A2, A5, MATRIX_3:def 4
.= 1 by A4, Def9 ;
thus (A + B) * x = Col (((A * (ColVec2Mx x)) + (B * (ColVec2Mx x))),1) by A1, A2, A5, MATRIX_4:63
.= (A * x) + (B * x) by A6, A7, Th54 ; :: thesis: verum