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 that
A1: len x = len A and
A2: len A = len B and
A3: width A = width B and
A4: len A > 0 ; :: thesis: x * (A - B) = (x * A) - (x * B)
A5: width (LineVec2Mx x) = len x by MATRIXR1:def 10;
then A6: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A1, MATRIX_3:def 4
.= 1 by MATRIXR1:def 10 ;
A7: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A1, A5, MATRIX_3:def 4
.= len ((LineVec2Mx x) * B) by A1, A2, A5, MATRIX_3:def 4 ;
A8: width ((LineVec2Mx x) * A) = width A by A1, A5, MATRIX_3:def 4
.= width ((LineVec2Mx x) * B) by A1, A2, A3, A5, MATRIX_3:def 4 ;
len (LineVec2Mx x) = 1 by MATRIXR1:def 10;
hence x * (A - B) = Line ((((LineVec2Mx x) * A) - ((LineVec2Mx x) * B)),1) by A1, A2, A3, A4, A5, Th20
.= (x * A) - (x * B) by A8, A7, A6, Th25 ;
:: thesis: verum