let n be Nat; :: thesis: for z1, z2 being Element of COMPLEX n holds
( |.(z1 - z2).| = 0 iff z1 = z2 )
let z1, z2 be Element of COMPLEX n; :: 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 = 0c n by Th93;
hence z1 = z2 by Th73; :: thesis: verum
end;
assume z1 = z2 ; :: thesis: |.(z1 - z2).| = 0
then z1 - z2 = 0c n by Th72;
hence |.(z1 - z2).| = 0 by Th92; :: thesis: verum