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