theorem :: COMPLEX1:69

for z being Complex holds |.(z * z).| = |.(z * (z *')).|