let z1, z2 be Complex; ( |.(z1 - z2).| = 0 iff z1 = z2 )
thus
( |.(z1 - z2).| = 0 implies z1 = z2 )
( z1 = z2 implies |.(z1 - z2).| = 0 )proof
assume
|.(z1 - z2).| = 0
;
z1 = z2
then
z1 - z2 = 0
;
hence
z1 = z2
;
verum
end;
thus
( z1 = z2 implies |.(z1 - z2).| = 0 )
; verum