let z1, z2 be Complex; :: thesis: ( |.(z1 - z2).| = 0 iff z1 = z2 )
thus ( |.(z1 - z2).| = 0 implies z1 = z2 ) :: thesis: ( z1 = z2 implies |.(z1 - z2).| = 0 )

proof

assume |.(z1 - z2).| = 0 ; :: thesis: z1 = z2
then z1 - z2 = 0 ;
hence z1 = z2 ; :: thesis: verum

end;

thus ( z1 = z2 implies |.(z1 - z2).| = 0 ) ; :: thesis: verum