theorem Th28: :: COMPLEX2:30

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