theorem Th31: :: MATRIXR2:31

for n, m being Nat
for A being Matrix of REAL st len A = n & width A = m holds
(- A) + A = 0_Rmatrix (n,m)