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