theorem Th5: :: COMPLEX1:5

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