theorem :: POLYNOM5:65

FPower ((1_ F_Complex),2) = (id COMPLEX) (#) (id COMPLEX)