let A, B be Matrix of REAL ; :: thesis: ( len A = len B & width A = width B & len A > 0 & A + B = 0_Rmatrix (len A),(width A) implies B = - A )
assume A1: ( len A = len B & width A = width B & len A > 0 & A + B = 0_Rmatrix (len A),(width A) ) ; :: thesis: B = - A
A2: ( 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 A1, MATRIX_4:1
.= (MXR2MXF A) - (- (MXR2MXF B)) by MATRIX_4:def 1 ;
then MXR2MXF A = - (MXR2MXF B) by A1, A2, MATRIX_4:7;
hence B = - A by MATRIX_4:1; :: thesis: verum