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