let A, B be Matrix of REAL; :: thesis: ( len A = len B & width A = width B & A = A + B implies B = 0_Rmatrix ((len A),(width A)) )
assume that
A1: ( len A = len B & width A = width B ) and
A2: A = A + B ; :: thesis: B = 0_Rmatrix ((len A),(width A))
0_Rmatrix ((len A),(width A)) = (A + B) + (- A) by A2, MATRIX_4:2
.= MXF2MXR (((MXR2MXF B) + (MXR2MXF A)) + (- (MXR2MXF A))) by A1, MATRIX_3:2
.= MXF2MXR (((MXR2MXF B) + (MXR2MXF A)) - (MXR2MXF A)) by MATRIX_4:def 1
.= B by A1, MATRIX_4:21 ;
hence B = 0_Rmatrix ((len A),(width A)) ; :: thesis: verum