let K be Field; :: thesis: for A, C being Matrix of K st len A = width C & len C > 0 & len A > 0 holds
(- C) * A = - (C * A)
let A, C be Matrix of K; :: thesis: ( len A = width C & len C > 0 & len A > 0 implies (- C) * A = - (C * A) )
assume A1: ( len A = width C & len C > 0 & len A > 0 ) ; :: thesis: (- C) * A = - (C * A)
A2: width (- C) = width C by MATRIX_3:def 2;
A3: len C = len (- C) by MATRIX_3:def 2;
A4: len (- C) = len ((- C) * A) by A1, A2, MATRIX_3:def 4;
A5: width ((- C) * A) = width A by A1, A2, MATRIX_3:def 4;
A6: ( len C = len (- C) & width (- C) = width C ) by MATRIX_3:def 2;
then A7: ( len ((- C) * A) = len (- C) & width ((- C) * A) = width A ) by A1, MATRIX_3:def 4;
A8: ( len (C * A) = len ((- C) * A) & width (C * A) = width ((- C) * A) ) by A1, A3, A4, A5, MATRIX_3:def 4;
reconsider D = C as Matrix of len C, width C,K by A1, MATRIX_1:20;
(C * A) + ((- C) * A) = (D + (- D)) * A by A1, A6, MATRIX_4:63
.= (0. K,(len C),(width C)) * A by MATRIX_3:7
.= 0. K,(len C),(width A) by A1, Th14 ;
hence (- C) * A = - (C * A) by A3, A7, A8, MATRIX_4:8; :: thesis: verum