let M1, M2 be Matrix of COMPLEX ; :: thesis: ( len M1 = len M2 & width M1 = width M2 & len M1 > 0 & M1 = M1 + M2 implies M2 = 0_Cx (len M1),(width M1) )
assume A1: ( len M1 = len M2 & width M1 = width M2 & len M1 > 0 & M1 = M1 + M2 ) ; :: thesis: M2 = 0_Cx (len M1),(width M1)
then 0_Cx (len M1),(width M1) = (M1 + M2) + (- M1) by MATRIX_4:2
.= Field2COMPLEX (((COMPLEX2Field M2) + (COMPLEX2Field M1)) - (COMPLEX2Field M1)) by A1, MATRIX_3:4
.= M2 by A1, MATRIX_4:21 ;
hence M2 = 0_Cx (len M1),(width M1) ; :: thesis: verum