let K be Ring; :: 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:64; :: thesis: verum

end;

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

( len (- M) = len M & width (- M) = width M ) by MATRIX_3:def 2;
then A3: - M is Matrix of len M, width M,K by A2, MATRIX_0:20;
M is Matrix of len M, width M,K by A2, MATRIX_0:20;
then A4: Indices (- M) = Indices M by A3, MATRIX_0:26;
A5: 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 A6: [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 A4, A6, MATRIX_3:def 2;
hence M * (i,j) = (- (- M)) * (i,j) by RLVECT_1:17; :: thesis: verum

end;

width (- (- M)) = width (- M) by MATRIX_3:def 2;
then A7: width (- (- M)) = width M by MATRIX_3:def 2;
len (- (- M)) = len (- M) by MATRIX_3:def 2;
then len (- (- M)) = len M by MATRIX_3:def 2;
hence - (- M) = M by A7, A5, MATRIX_0:21; :: thesis: verum

end;

end;