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 A > 0 & 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 A > 0 & len x > 0 implies (A + B) * x = (A * x) + (B * x) )
assume A1: ( len A = len B & width A = width B & width A = len x & len A > 0 & len x > 0 ) ; :: thesis: (A + B) * x = (A * x) + (B * x)
then A2: len (ColVec2Mx x) = len x by Def9;
then A3: len (A * (ColVec2Mx x)) = len A by A1, MATRIX_3:def 4
.= len (B * (ColVec2Mx x)) by A1, A2, MATRIX_3:def 4 ;
A4: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A1, A2, MATRIX_3:def 4
.= width (B * (ColVec2Mx x)) by A1, A2, MATRIX_3:def 4 ;
A5: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A1, A2, MATRIX_3:def 4
.= 1 by A1, Def9 ;
thus (A + B) * x = Col ((A * (ColVec2Mx x)) + (B * (ColVec2Mx x))),1 by A1, A2, MATRIX_4:63
.= (A * x) + (B * x) by A3, A4, A5, Th54 ; :: thesis: verum