theorem Th8: :: HERMITAN:8

for a being Element of F_Complex ex b being Element of F_Complex st
( |.b.| = 1 & Re (b * a) = |.a.| & Im (b * a) = 0 )