let z be complex number ; :: thesis: ( |.z.| = 0 implies z = 0 )
assume |.z.| = 0 ; :: thesis: z = 0
then ((Re z) ^2 ) + ((Im z) ^2 ) = 0 by Lm2, SQUARE_1:92;
hence z = 0 by Th13; :: thesis: verum