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

( 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