let x be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st len x = width A & len A > 0 & len x > 0 holds
(- A) * x = - (A * x)
let A be Matrix of REAL ; :: thesis: ( len x = width A & len A > 0 & len x > 0 implies (- A) * x = - (A * x) )
assume A1: ( len x = width A & len A > 0 & len x > 0 ) ; :: thesis: (- A) * x = - (A * x)
then A2: len (ColVec2Mx x) = len x by MATRIXR1:def 9;
A3: width (ColVec2Mx x) = 1 by A1, MATRIXR1:def 9;
then A4: 1 <= width (A * (ColVec2Mx x)) by A1, A2, MATRIX_3:def 4;
thus (- A) * x = Col (((- 1) * A) * (ColVec2Mx x)),1 by Th9
.= Col ((- 1) * (A * (ColVec2Mx x))),1 by A1, A2, A3, MATRIXR1:41
.= - (A * x) by A4, MATRIXR1:56 ; :: thesis: verum