let n, m be Element of NAT ; :: thesis: for K being Field holds - (0. K,n,m) = 0. K,n,m
let K be Field; :: 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:6;
A3: len (0. K,n,m) = n by MATRIX_1:def 3;
then width (0. K,n,m) = m by A1, MATRIX_1: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 by FINSEQ_1:def 18;
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:83; :: thesis: verum

end;

end;