theorem Th7: :: COMPLFLD:7

0. F_Complex = 0c by Def1;