for i being Integer
for c being Element of F_Complex
for f being FinSequence of the carrier of (Polynom-Ring F_Complex)
for p being Polynomial of F_Complex st p = Product f & c = i & ( for i being non zero Element of NAT holds
( not i in dom f or f . i = <%(1_ F_Complex)%> or f . i = cyclotomic_poly i ) ) holds
eval (p,c) is integer