let A, B be Matrix of REAL ; :: thesis: ( len A = len B & width A = width B & len A > 0 & B - A = B implies A = 0_Rmatrix (len A),(width A) )
assume A1: ( len A = len B & width A = width B & len A > 0 & B - A = B ) ; :: thesis: A = 0_Rmatrix (len A),(width A)
then (MXR2MXF B) + (MXR2MXF A) = MXR2MXF B by MATRIX_4:22;
hence A = 0_Rmatrix (len A),(width A) by A1, MATRIX_4:6; :: thesis: verum