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