theorem Th12: :: COMSEQ_3:12

for z being Complex holds |.z.| <= |.(Re z).| + |.(Im z).|