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 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;

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;

end;

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;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