let n, m be 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:2
.= 0_Rmatrix (n,m) by A1, MATRIX_4:2 ;
:: thesis: verum