theorem Th13: :: HERMITAN:13

for a being Element of F_Complex holds a * (a *') = |.a.| ^2