let n be non empty 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;
i is Real by A1, XREAL_0:def 1;
then consider y being Element of F_Complex such that
A2: y = i and
A3: eval (unital_poly F_Complex ,n),y = (j |^ n) - 1 by Th48;
thus eval (unital_poly F_Complex ,n),i is Integer by A2, A3; :: thesis: verum