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