let A, B be Matrix of REAL; :: thesis: ( len A = len B & width A = width B & len A > 0 implies A + (B - B) = A )
assume A1: ( len A = len B & width A = width B ) ; :: thesis: ( not len A > 0 or A + (B - B) = A )
assume len A > 0 ; :: thesis: A + (B - B) = A
hence A = A + (0_Rmatrix ((len B),(width B))) by A1, MATRIXR1:36
.= (MXF2MXR (MXR2MXF A)) + (MXF2MXR ((MXR2MXF B) + (- (MXR2MXF B)))) by MATRIX_4:2
.= A + (B - B) by MATRIX_4:def 1 ;
:: thesis: verum