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

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