let n be non zero Element of NAT ; :: thesis: for i being Element of F_Complex st i is Integer holds
eval ((unital_poly (F_Complex,n)),i) is Integer
let i be Element of F_Complex; :: thesis: ( i is Integer implies eval ((unital_poly (F_Complex,n)),i) is Integer )
assume A1: i is Integer ; :: thesis: eval ((unital_poly (F_Complex,n)),i) is Integer
reconsider j = i as Integer by A1;
ex y being Element of F_Complex st
( y = i & eval ((unital_poly (F_Complex,n)),y) = (j |^ n) - 1 ) by Th44;
hence eval ((unital_poly (F_Complex,n)),i) is Integer ; :: thesis: verum