for z being Element of F_Complex holds
( z <> 0. F_Complex iff 0 < |.z.| ) by Th7, COMPLEX1:47;