theorem :: HERMITAN:6

i_FC * (i_FC *') = 1_ F_Complex by COMPLEX1:7, COMPLFLD:8;