theorem :: COMPLFLD:58

for z being Element of F_Complex st |.z.| = 0 holds
z = 0. F_Complex by Th7;