for n, m being Nat st n > 0 holds
(0_Rmatrix (n,m)) + (0_Rmatrix (n,m)) = 0_Rmatrix (n,m)