let K be Field; :: 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 & width (- M) = width M ) by MATRIX_3:def 2;
A2: len (0. K,(len M),(width M)) = len M by MATRIX_1:def 3;

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

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

then A4: width (0. K,(len M),(width M)) = width M by A2, MATRIX_1:20;
A5: - M is Matrix of len M, width M,K by A1, A3, MATRIX_1:20;
(0. K,(len M),(width M)) - M = (- M) + (0. K,(len M),(width M)) by A1, A2, A4, MATRIX_3:4;
hence (0. K,(len M),(width M)) - M = - M by A5, MATRIX_3:6; :: 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, A2, A6, CARD_2:83; :: thesis: verum

end;

end;