theorem :: COMPLFLD:8

1_ F_Complex = 1r by Def1;