thus i_FC * i_FC = - 1r
.= - (1_ F_Complex) by COMPLFLD:4, COMPLFLD:10 ; :: thesis: verum