let A, B be Matrix of REAL; :: thesis: ( len A = len B & width A = width B & A + B = 0_Rmatrix ((len A),(width A)) implies B = - A )
assume that
A1: ( len A = len B & width A = width B ) and
A2: A + B = 0_Rmatrix ((len A),(width A)) ; :: thesis: B = - A
A3: ( len (- (MXR2MXF B)) = len (MXR2MXF B) & width (- (MXR2MXF B)) = width (MXR2MXF B) ) by MATRIX_3:def 2;
MXR2MXF (0_Rmatrix ((len A),(width A))) = (MXR2MXF A) + (- (- (MXR2MXF B))) by A2, MATRIX_4:1
.= (MXR2MXF A) - (- (MXR2MXF B)) by MATRIX_4:def 1 ;
then MXR2MXF A = - (MXR2MXF B) by A1, A3, MATRIX_4:7;
hence B = - A by MATRIX_4:1; :: thesis: verum