let M be Matrix of COMPLEX; :: thesis: M + (0_Cx ((len M),(width M))) = M
A1: ( len M = len (COMPLEX2Field M) & width M = width (COMPLEX2Field M) ) ;
M + (0_Cx ((len M),(width M))) = M + (- (0_Cx ((len M),(width M)))) by MATRIX_4:9
.= Field2COMPLEX ((COMPLEX2Field M) - ((COMPLEX2Field M) - (COMPLEX2Field M))) by MATRIX_4:3
.= M by A1, MATRIX_4:11 ;
hence M + (0_Cx ((len M),(width M))) = M ; :: thesis: verum