let x, y be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st len x = len A & len y = len x & len x > 0 holds
(x - y) * A = (x * A) - (y * A)
let A be Matrix of REAL; :: thesis: ( len x = len A & len y = len x & len x > 0 implies (x - y) * A = (x * A) - (y * A) )
assume that
A1: len x = len A and
A2: len y = len x and
A3: len x > 0 ; :: thesis: (x - y) * A = (x * A) - (y * A)
A4: width (LineVec2Mx y) = len y by MATRIXR1:def 10;
A5: width (LineVec2Mx x) = len x by MATRIXR1:def 10;
then A6: width ((LineVec2Mx x) * A) = width A by A1, MATRIX_3:def 4
.= width ((LineVec2Mx y) * A) by A1, A2, A4, MATRIX_3:def 4 ;
A7: len (LineVec2Mx y) = 1 by MATRIXR1:def 10;
A8: len (LineVec2Mx x) = 1 by MATRIXR1:def 10;
then A9: 1 <= len ((LineVec2Mx x) * A) by A1, A5, MATRIX_3:def 4;
A10: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A1, A5, MATRIX_3:def 4
.= len (LineVec2Mx y) by A7, MATRIXR1:def 10
.= len ((LineVec2Mx y) * A) by A1, A2, A4, MATRIX_3:def 4 ;
thus (x - y) * A = Line ((((LineVec2Mx x) - (LineVec2Mx y)) * A),1) by A2, Th23
.= Line ((((LineVec2Mx x) * A) - ((LineVec2Mx y) * A)),1) by A1, A2, A3, A5, A4, A8, A7, Th16
.= (x * A) - (y * A) by A6, A10, A9, Th25 ; :: thesis: verum