theorem :: COMPLEX1:40

for z being Complex holds
( Re (z * (z *')) = ((Re z) ^2) + ((Im z) ^2) & Im (z * (z *')) = 0 )