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 A1: ( len x = width A & len A = len B & width A = width B & len x > 0 & len A > 0 ) ; :: thesis: (A - B) * x = (A * x) - (B * x)
then A2: len (ColVec2Mx x) = len x by MATRIXR1:def 9;
then A3: len (A * (ColVec2Mx x)) = len A by A1, MATRIX_3:def 4
.= len (B * (ColVec2Mx x)) by A1, A2, MATRIX_3:def 4 ;
A4: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A1, A2, MATRIX_3:def 4
.= width (B * (ColVec2Mx x)) by A1, A2, MATRIX_3:def 4 ;
A5: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A1, A2, MATRIX_3:def 4
.= 1 by A1, MATRIXR1:45 ;
thus (A - B) * x = Col ((A * (ColVec2Mx x)) - (B * (ColVec2Mx x))),1 by A1, A2, Th16
.= (A * x) - (B * x) by A3, A4, A5, Th26 ; :: thesis: verum