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