let n be non empty Element of NAT ; :: thesis: Roots (unital_poly F_Complex ,n) = n -roots_of_1

now

set p = unital_poly F_Complex ,n;
let x be set ; :: thesis: ( ( x in Roots (unital_poly F_Complex ,n) implies x in n -roots_of_1 ) & ( x in n -roots_of_1 implies x in Roots (unital_poly F_Complex ,n) ) )

hereby :: thesis: ( x in n -roots_of_1 implies x in Roots (unital_poly F_Complex ,n) )

assume A1: x in Roots (unital_poly F_Complex ,n) ; :: thesis: x in n -roots_of_1
then reconsider x9 = x as Element of F_Complex ;
x9 is_a_root_of unital_poly F_Complex ,n by A1, POLYNOM5:def 9;
then 0. F_Complex = eval (unital_poly F_Complex ,n),x9 by POLYNOM5:def 6
.= ((power F_Complex ) . x9,n) - 1 by Th45 ;
then x9 is CRoot of n, 1_ F_Complex by COMPLFLD:9, COMPLFLD:10, COMPLFLD:def 2;
hence x in n -roots_of_1 ; :: thesis: verum

end;

assume A2: x in n -roots_of_1 ; :: thesis: x in Roots (unital_poly F_Complex ,n)
then reconsider x9 = x as Element of F_Complex ;
x9 is CRoot of n, 1_ F_Complex by A2, Th24;
then (power F_Complex ) . x9,n = 1 by COMPLFLD:10, COMPLFLD:def 2;
then ((power F_Complex ) . x9,n) - 1 = 0c ;
then eval (unital_poly F_Complex ,n),x9 = 0. F_Complex by Th45, COMPLFLD:9;
then x9 is_a_root_of unital_poly F_Complex ,n by POLYNOM5:def 6;
hence x in Roots (unital_poly F_Complex ,n) by POLYNOM5:def 9; :: thesis: verum

end;

hence Roots (unital_poly F_Complex ,n) = n -roots_of_1 by TARSKI:2; :: thesis: verum