let K be Ring; :: thesis: for M being Matrix of K holds (0. (K,(len M),(width M))) - M = - M
let M be Matrix of K; :: thesis: (0. (K,(len M),(width M))) - M = - M
A1: len (- M) = len M by MATRIX_3:def 2;
A2: width (- M) = width M by MATRIX_3:def 2;
A3: len (0. (K,(len M),(width M))) = len M by MATRIX_0:def 2;

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

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

then width (0. (K,(len M),(width M))) = width M by A3, MATRIX_0:20;
then A5: (0. (K,(len M),(width M))) - M = (- M) + (0. (K,(len M),(width M))) by A1, A2, A3, MATRIX_3:2;
- M is Matrix of len M, width M,K by A1, A2, A4, MATRIX_0:20;
hence (0. (K,(len M),(width M))) - M = - M by A5, MATRIX_3:4; :: thesis: verum

end;

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

len ((0. (K,(len M),(width M))) - M) = len (0. (K,(len M),(width M))) by MATRIX_3:def 3;
hence (0. (K,(len M),(width M))) - M = - M by A1, A3, A6, CARD_2:64; :: thesis: verum

end;

end;