theorem :: COMPLEX1:45

for z being Complex st |.z.| = 0 holds
z = 0 ;