theorem :: HERMITAN:5

for a being Element of F_Complex st a = a *' holds
Im a = 0 by Th1;