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 that
A1: ( len A = len B & width A = width B ) and
A2: len A > 0 ; :: thesis: (A + B) - B = A
thus (A + B) - B = (A + B) + (- B) by MATRIX_4:def 1
.= A + (B + (- B)) by A1, MATRIX_3:3
.= A + (B - B) by MATRIX_4:def 1
.= A by A1, A2, Th7 ; :: thesis: verum