theorem Th3: :: HAHNBAN1:4

i_FC * i_FC = - (1_ F_Complex)