theorem Th41: :: UNIROOTS:41

for n being non zero Element of NAT
for x being Element of F_Complex holds eval ((unital_poly (F_Complex,n)),x) = ((power F_Complex) . (x,n)) - 1