let K be Field; :: thesis: for M being Matrix of K holds - (- M) = M
let M be Matrix of K; :: thesis: - (- M) = M

per cases ( len M = 0 or len M > 0 ) by NAT_1:3;

suppose A1: len M = 0 ; :: thesis: - (- M) = M

then len (- M) = 0 by MATRIX_3:def 2;
then len (- (- M)) = 0 by MATRIX_3:def 2;
hence - (- M) = M by A1, CARD_2:83; :: thesis: verum

end;

suppose A2: len M > 0 ; :: thesis: - (- M) = M

A3: ( len (- M) = len M & width (- M) = width M ) by MATRIX_3:def 2;
( len (- (- M)) = len (- M) & width (- (- M)) = width (- M) ) by MATRIX_3:def 2;
then A4: ( len (- (- M)) = len M & width (- (- M)) = width M ) by MATRIX_3:def 2;
A5: M is Matrix of len M, width M,K by A2, MATRIX_1:20;
- M is Matrix of len M, width M,K by A2, A3, MATRIX_1:20;
then A6: Indices (- M) = Indices M by A5, MATRIX_1:27;
for i, j being Nat st [i,j] in Indices M holds
M * i,j = (- (- M)) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M * i,j = (- (- M)) * i,j )
assume A7: [i,j] in Indices M ; :: thesis: M * i,j = (- (- M)) * i,j
then (- M) * i,j = - (M * i,j) by MATRIX_3:def 2;
then (- (- M)) * i,j = - (- (M * i,j)) by A6, A7, MATRIX_3:def 2;
hence M * i,j = (- (- M)) * i,j by RLVECT_1:30; :: thesis: verum

end;

hence - (- M) = M by A4, MATRIX_1:21; :: thesis: verum

end;

end;