let x1, x2 be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st len x1 = len x2 & len A = len x1 & len x1 > 0 holds
(x1 + x2) * A = (x1 * A) + (x2 * A)
let A be Matrix of REAL ; :: thesis: ( len x1 = len x2 & len A = len x1 & len x1 > 0 implies (x1 + x2) * A = (x1 * A) + (x2 * A) )
assume A1: ( len x1 = len x2 & len A = len x1 & len x1 > 0 ) ; :: thesis: (x1 + x2) * A = (x1 * A) + (x2 * A)
A2: width (LineVec2Mx x1) = len x1 by Def10;
A3: width (LineVec2Mx x2) = len x2 by Def10;
A4: len (LineVec2Mx x1) = 1 by Def10;
A5: len (LineVec2Mx x2) = 1 by Def10;
A6: width ((LineVec2Mx x1) * A) = width A by A1, A2, MATRIX_3:def 4
.= width ((LineVec2Mx x2) * A) by A1, A3, MATRIX_3:def 4 ;
A7: len ((LineVec2Mx x1) * A) = len (LineVec2Mx x1) by A1, A2, MATRIX_3:def 4
.= len (LineVec2Mx x2) by A5, Def10
.= len ((LineVec2Mx x2) * A) by A1, A3, MATRIX_3:def 4 ;
A8: 1 <= len ((LineVec2Mx x1) * A) by A1, A2, A4, MATRIX_3:def 4;
thus (x1 + x2) * A = Line (((LineVec2Mx x1) + (LineVec2Mx x2)) * A),1 by A1, Th50
.= Line (((LineVec2Mx x1) * A) + ((LineVec2Mx x2) * A)),1 by A1, A2, A3, A4, A5, MATRIX_4:63
.= (x1 * A) + (x2 * A) by A6, A7, A8, Th55 ; :: thesis: verum