theorem :: MATRIXR1:37

for A, B being Matrix of REAL st len A = len B & width A = width B & A = A + B holds
B = 0_Rmatrix ((len A),(width A))