theorem :: MATRIXR1:39
for A, B being Matrix of REAL st len A = len B & width A = width B & B - A = B holds
A = 0_Rmatrix ((len A),(width A))