theorem :: COMPLFLD:47

(0. F_Complex) *' = 0. F_Complex