let z1, z2 be Element of F_Complex; :: thesis: ( |.(z1 - z2).| = 0 iff z1 = z2 )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
thus ( |.(z1 - z2).| = 0 implies z1 = z2 ) :: thesis: ( z1 = z2 implies |.(z1 - z2).| = 0 )

proof

assume A1: |.(z1 - z2).| = 0 ; :: thesis: z1 = z2
z1 - z2 = z19 - z29 by Th3;
hence z1 = z2 by A1, COMPLEX1:61; :: thesis: verum

end;

assume A2: z1 = z2 ; :: thesis: |.(z1 - z2).| = 0
z19 - z29 = z1 - z2 by Th3;
hence |.(z1 - z2).| = 0 by A2; :: thesis: verum