let x1, x2 be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st len x1 = len x2 & width A = len x1 & len x1 > 0 & len A > 0 holds
A * (x1 + x2) = (A * x1) + (A * x2)
let A be Matrix of REAL ; :: thesis: ( len x1 = len x2 & width A = len x1 & len x1 > 0 & len A > 0 implies A * (x1 + x2) = (A * x1) + (A * x2) )
assume A1: ( len x1 = len x2 & width A = len x1 & len x1 > 0 & len A > 0 ) ; :: thesis: A * (x1 + x2) = (A * x1) + (A * x2)
then A2: len (ColVec2Mx x1) = len x1 by Def9;
A3: len (ColVec2Mx x2) = len x2 by A1, Def9;
A4: width (ColVec2Mx x1) = 1 by A1, Def9;
A5: width (ColVec2Mx x2) = 1 by A1, Def9;
A6: len (A * (ColVec2Mx x1)) = len A by A1, A2, MATRIX_3:def 4
.= len (A * (ColVec2Mx x2)) by A1, A3, MATRIX_3:def 4 ;
A7: width (A * (ColVec2Mx x1)) = width (ColVec2Mx x1) by A1, A2, MATRIX_3:def 4
.= width (ColVec2Mx x2) by A1, A5, Def9
.= width (A * (ColVec2Mx x2)) by A1, A3, MATRIX_3:def 4 ;
A8: ( 1 <= 1 & 1 <= width (A * (ColVec2Mx x1)) ) by A1, A2, A4, MATRIX_3:def 4;
thus A * (x1 + x2) = Col (A * ((ColVec2Mx x1) + (ColVec2Mx x2))),1 by A1, Th46
.= Col ((A * (ColVec2Mx x1)) + (A * (ColVec2Mx x2))),1 by A1, A2, A3, A4, A5, MATRIX_4:62
.= (A * x1) + (A * x2) by A6, A7, A8, Th54 ; :: thesis: verum