theorem Th4: :: HERMITAN:4

for a being Element of COMPLEX holds a * (a *') = (|.a.| ^2) + (0 * <i>)