let M be Matrix of REAL; :: thesis: M + (0_Rmatrix ((len M),(width M))) = M
A1: ( len M = len (MXR2MXF M) & width M = width (MXR2MXF M) ) ;
M + (0_Rmatrix ((len M),(width M))) = M + (- (0_Rmatrix ((len M),(width M)))) by MATRIX_4:9
.= M + (- (M - M)) by MATRIX_4:3
.= MXF2MXR ((MXR2MXF M) - ((MXR2MXF M) - (MXR2MXF M))) by MATRIX_4:def 1
.= M by A1, MATRIX_4:11 ;
hence M + (0_Rmatrix ((len M),(width M))) = M ; :: thesis: verum