let A, B be Matrix of REAL; :: thesis: A - (- B) = A + B
A + B = MXF2MXR ((MXR2MXF A) + (MXR2MXF (- (- B)))) by MATRIX_4:1;
hence A - (- B) = A + B by MATRIX_4:def 1; :: thesis: verum