theorem Th29: :: COMPLEX2:31

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