theorem :: COMPLFLD:17

(1. F_Complex) " = 1. F_Complex