theorem :: HERMITAN:11

for a, b being Element of F_Complex st Im a = 0 & Im b = 0 holds
Im (a * b) = 0