let x be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st len x = len A & len x > 0 & width A > 0 holds
x * (- A) = - (x * A)
let A be Matrix of REAL ; :: thesis: ( len x = len A & len x > 0 & width A > 0 implies x * (- A) = - (x * A) )
assume A1: ( len x = len A & len x > 0 & width A > 0 ) ; :: thesis: x * (- A) = - (x * A)
A2: ( len A = len (- A) & width A = width (- A) ) by MATRIX_3:def 2;
then A3: (x * (- A)) + (x * A) = x * ((- A) + A) by A1, MATRIXR1:64
.= x * (0_Rmatrix (len A),(width A)) by A1, Th31
.= 0* (width A) by A1, MATRIXR1:66 ;
A4: len (x * (- A)) = width A by A1, A2, MATRIXR1:62;
width A = len (x * A) by A1, MATRIXR1:62;
hence x * (- A) = - (x * A) by A3, A4, Th1; :: thesis: verum