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 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 implies A * (x1 + x2) = (A * x1) + (A * x2) )
assume that
A1: len x1 = len x2 and
A2: width A = len x1 and
A3: len x1 > 0 ; :: thesis: A * (x1 + x2) = (A * x1) + (A * x2)
A5: len (ColVec2Mx x2) = len x2 by A1, A3, Def9;
A6: len (ColVec2Mx x1) = len x1 by A3, Def9;
then A7: len (A * (ColVec2Mx x1)) = len A by A2, MATRIX_3:def 4
.= len (A * (ColVec2Mx x2)) by A1, A2, A5, MATRIX_3:def 4 ;
A8: width (ColVec2Mx x1) = 1 by A3, Def9;
then A9: 1 <= width (A * (ColVec2Mx x1)) by A2, A6, MATRIX_3:def 4;
A10: width (ColVec2Mx x2) = 1 by A1, A3, Def9;
thus A * (x1 + x2) = Col ((A * ((ColVec2Mx x1) + (ColVec2Mx x2))),1) by A1, A3, Th46
.= Col (((A * (ColVec2Mx x1)) + (A * (ColVec2Mx x2))),1) by A1, A2, A6, A5, A8, A10, MATRIX_4:62
.= (A * x1) + (A * x2) by A7, A9, Th54 ; :: thesis: verum