for z being Complex holds
( z = 0 iff ((Re z) ^2) + ((Im z) ^2) = 0 ) by Th4, Th1;