theorem Th3: :: COMPTRIG:3

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