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