let K be Ring; :: 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_0:20;
hence M + (- M) = 0. (K,(len M),(width M)) by MATRIX_3:5; :: 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;
hence M + (- M) = 0. (K,(len M),(width M)) by A1, A2, CARD_2:64; :: thesis: verum

end;

end;