let K be Field; :: thesis: for M being Matrix of K holds M + (- M) = 0. K,(len M),(width M)
let M be Matrix of K; :: thesis: M + (- M) = 0. K,(len M),(width M)

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

suppose len M > 0 ; :: thesis: M + (- M) = 0. K,(len M),(width M)

then M is Matrix of len M, width M,K by MATRIX_1:20;
hence M + (- M) = 0. K,(len M),(width M) by MATRIX_3:7; :: thesis: verum

end;

suppose A1: len M = 0 ; :: thesis: M + (- M) = 0. K,(len M),(width M)

A2: len (M + (- M)) = len M by MATRIX_3:def 3;
len (0. K,(len M),(width M)) = 0 by A1, FINSEQ_1:def 18;
hence M + (- M) = 0. K,(len M),(width M) by A1, A2, CARD_2:83; :: thesis: verum

end;

end;