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