let A, B be Matrix of REAL ; :: thesis: ( len A = len B & width A = width B & len A > 0 & A = A + B implies B = 0_Rmatrix (len A),(width A) )
assume A1: ( len A = len B & width A = width B & len A > 0 & A = A + B ) ; :: thesis: B = 0_Rmatrix (len A),(width A)
then 0_Rmatrix (len A),(width A) = (A + B) + (- A) by MATRIX_4:2
.= MXF2MXR (((MXR2MXF B) + (MXR2MXF A)) + (- (MXR2MXF A))) by A1, MATRIX_3:4
.= 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