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 Th5;
hence z1 = z2 by A1, COMPLEX1:147; :: thesis: verum

end;

assume A2: z1 = z2 ; :: thesis: |.(z1 - z2).| = 0
z19 - z29 = z1 - z2 by Th5;
hence |.(z1 - z2).| = 0 by A2, COMPLEX1:147; :: thesis: verum