theorem :: HURWITZ2:2

for a being Complex holds a * (a *') = |.a.| ^2