let n be non zero Element of NAT ; :: thesis: for x being Real ex y being Element of F_Complex st
( y = x & eval ((unital_poly (F_Complex,n)),y) = (x |^ n) - 1 )
let x be Real; :: thesis: ex y being Element of F_Complex st
( y = x & eval ((unital_poly (F_Complex,n)),y) = (x |^ n) - 1 )
x in COMPLEX by XCMPLX_0:def 2;
then reconsider y = x as Element of F_Complex by COMPLFLD:def 1;
ex x2 being Real st
( x2 = y & (power F_Complex) . (y,n) = x2 |^ n ) by Th43;
then eval ((unital_poly (F_Complex,n)),y) = (x |^ n) - 1 by Th41;
hence ex y being Element of F_Complex st
( y = x & eval ((unital_poly (F_Complex,n)),y) = (x |^ n) - 1 ) ; :: thesis: verum