for n being non zero Element of NAT
for x being Real ex y being Element of F_Complex st
( y = x & eval ((unital_poly (F_Complex,n)),y) = (x |^ n) - 1 )