theorem :: COMPLEX1:16

for z being Complex holds
( Re (z * z) = ((Re z) ^2) - ((Im z) ^2) & Im (z * z) = 2 * ((Re z) * (Im z)) )