theorem :: COMPLFLD:60

|.(1. F_Complex).| = 1 by Def1, COMPLEX1:48;