theorem Th36: :: MATRIXR1:36
for n, m being Nat
for A being Matrix of REAL st len A = n & width A = m & n > 0 holds
( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A )