let n, m be Nat; :: thesis: for K being Ring holds - (0. (K,n,m)) = 0. (K,n,m)
let K be Ring; :: thesis: - (0. (K,n,m)) = 0. (K,n,m)

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

suppose A1: n > 0 ; :: thesis: - (0. (K,n,m)) = 0. (K,n,m)

A2: (0. (K,n,m)) + (0. (K,n,m)) = 0. (K,n,m) by MATRIX_3:4;
A3: len (0. (K,n,m)) = n by MATRIX_0:def 2;
then width (0. (K,n,m)) = m by A1, MATRIX_0:20;
hence - (0. (K,n,m)) = 0. (K,n,m) by A3, A2, Th8; :: thesis: verum

end;

suppose n = 0 ; :: thesis: - (0. (K,n,m)) = 0. (K,n,m)

then A4: len (0. (K,n,m)) = 0 ;
then len (- (0. (K,n,m))) = 0 by MATRIX_3:def 2;
hence - (0. (K,n,m)) = 0. (K,n,m) by A4, CARD_2:64; :: thesis: verum

end;

end;