let x1, x2 be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st len x1 = len x2 & len A = len x1 holds
(x1 + x2) * A = (x1 * A) + (x2 * A)
let A be Matrix of REAL; :: thesis: ( len x1 = len x2 & len A = len x1 implies (x1 + x2) * A = (x1 * A) + (x2 * A) )
assume that
A1: len x1 = len x2 and
A2: len A = len x1 ; :: thesis: (x1 + x2) * A = (x1 * A) + (x2 * A)
A4: width (LineVec2Mx x2) = len x2 by Def10;
A5: width (LineVec2Mx x1) = len x1 by Def10;
then A6: width ((LineVec2Mx x1) * A) = width A by A2, MATRIX_3:def 4
.= width ((LineVec2Mx x2) * A) by A1, A2, A4, MATRIX_3:def 4 ;
A7: len (LineVec2Mx x1) = 1 by Def10;
then A8: 1 <= len ((LineVec2Mx x1) * A) by A2, A5, MATRIX_3:def 4;
A9: len (LineVec2Mx x2) = 1 by Def10;
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, A5, A4, A7, A9, MATRIX_4:63
.= (x1 * A) + (x2 * A) by A6, A8, Th55 ; :: thesis: verum