let M1, M2 be Matrix of COMPLEX ; :: thesis: ( len M1 = len M2 & width M1 = width M2 & len M1 > 0 & M2 - M1 = M2 implies M1 = 0_Cx (len M1),(width M1) )
assume A1: ( len M1 = len M2 & width M1 = width M2 & len M1 > 0 & M2 - M1 = M2 ) ; :: thesis: M1 = 0_Cx (len M1),(width M1)
then (COMPLEX2Field M2) + (COMPLEX2Field M1) = COMPLEX2Field M2 by MATRIX_4:22;
hence M1 = 0_Cx (len M1),(width M1) by A1, MATRIX_4:6; :: thesis: verum