let x be FinSequence of REAL ; :: thesis: for A, B being Matrix of REAL st len x = width A & len A = len B & width A = width B & len x > 0 & len A > 0 holds
(A - B) * x = (A * x) - (B * x)
let A, B be Matrix of REAL; :: thesis: ( len x = width A & len A = len B & width A = width B & len x > 0 & len A > 0 implies (A - B) * x = (A * x) - (B * x) )
assume that
A1: len x = width A and
A2: len A = len B and
A3: width A = width B and
A4: len x > 0 and
A5: len A > 0 ; :: thesis: (A - B) * x = (A * x) - (B * x)
A6: len (ColVec2Mx x) = len x by A4, MATRIXR1:def 9;
then A7: len (A * (ColVec2Mx x)) = len A by A1, MATRIX_3:def 4
.= len (B * (ColVec2Mx x)) by A1, A2, A3, A6, MATRIX_3:def 4 ;
A8: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A1, A6, MATRIX_3:def 4
.= 1 by A4, MATRIXR1:45 ;
A9: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A1, A6, MATRIX_3:def 4
.= width (B * (ColVec2Mx x)) by A1, A3, A6, MATRIX_3:def 4 ;
thus (A - B) * x = Col (((A * (ColVec2Mx x)) - (B * (ColVec2Mx x))),1) by A1, A2, A3, A4, A5, A6, Th16
.= (A * x) - (B * x) by A7, A9, A8, Th26 ; :: thesis: verum