let n, m be Element of NAT ; :: thesis: for A being Matrix of REAL st len A = n & width A = m holds
(- A) + A = 0_Rmatrix n,m
let A be Matrix of REAL ; :: thesis: ( len A = n & width A = m implies (- A) + A = 0_Rmatrix n,m )
assume A1: ( len A = n & width A = m ) ; :: thesis: (- A) + A = 0_Rmatrix n,m
( len (- (MXR2MXF A)) = len A & width (- (MXR2MXF A)) = width A ) by MATRIX_3:def 2;
hence (- A) + A = MXF2MXR ((MXR2MXF A) + (- (MXR2MXF A))) by MATRIX_3:4
.= 0_Rmatrix n,m by A1, MATRIX_4:2 ;
:: thesis: verum