theorem :: COMPLFLD:67

for z1, z2 being Element of F_Complex holds
( |.(z1 - z2).| = 0 iff z1 = z2 ) by COMPLEX1:61;