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

now :: thesis: for x being set holds
( ( 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)) ) )

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 Th41 ;
then x9 is CRoot of n, 1_ F_Complex by COMPLFLD:7, COMPLFLD:8, 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, Th21;
then (power F_Complex) . (x9,n) = 1 by COMPLFLD:8, COMPLFLD:def 2;
then ((power F_Complex) . (x9,n)) - 1 = 0c ;
then eval ((unital_poly (F_Complex,n)),x9) = 0. F_Complex by Th41, COMPLFLD:7;
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:1; :: thesis: verum