let n be non zero Element of NAT ; 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; ( i is Integer implies eval ((unital_poly (F_Complex,n)),i) is Integer )
assume A1:
i is Integer
; 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
; verum