theorem :: COMPLEX1:68

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