let x be FinSequence of REAL ; :: thesis: for A, B being Matrix of REAL st len x = len A & len A = len B & width A = width B & len A > 0 holds
x * (A - B) = (x * A) - (x * B)
let A, B be Matrix of REAL ; :: thesis: ( len x = len A & len A = len B & width A = width B & len A > 0 implies x * (A - B) = (x * A) - (x * B) )
assume A1: ( len x = len A & len A = len B & width A = width B & len A > 0 ) ; :: thesis: x * (A - B) = (x * A) - (x * B)
A2: width (LineVec2Mx x) = len x by MATRIXR1:def 10;
A3: len (LineVec2Mx x) = 1 by MATRIXR1:def 10;
A4: width ((LineVec2Mx x) * A) = width A by A1, A2, MATRIX_3:def 4
.= width ((LineVec2Mx x) * B) by A1, A2, MATRIX_3:def 4 ;
A5: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A1, A2, MATRIX_3:def 4
.= len ((LineVec2Mx x) * B) by A1, A2, MATRIX_3:def 4 ;
A6: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A1, A2, MATRIX_3:def 4
.= 1 by MATRIXR1:def 10 ;
thus x * (A - B) = Line (((LineVec2Mx x) * A) - ((LineVec2Mx x) * B)),1 by A1, A2, A3, Th20
.= (x * A) - (x * B) by A4, A5, A6, Th25 ; :: thesis: verum