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

now :: thesis: for x being object 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)) ) )

hence
Roots (unital_poly (F_Complex,n)) = n -roots_of_1
by TARSKI:2; :: thesis: verum( ( 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 object ; :: 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)) ) )

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 7;

hence x in Roots (unital_poly (F_Complex,n)) by POLYNOM5:def 10; :: thesis: verum

end;let x be object ; :: 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 A2:
x in n -roots_of_1
; :: thesis: 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 10;

then 0. F_Complex = eval ((unital_poly (F_Complex,n)),x9) by POLYNOM5:def 7

.= ((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;then reconsider x9 = x as Element of F_Complex ;

x9 is_a_root_of unital_poly (F_Complex,n) by A1, POLYNOM5:def 10;

then 0. F_Complex = eval ((unital_poly (F_Complex,n)),x9) by POLYNOM5:def 7

.= ((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

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 7;

hence x in Roots (unital_poly (F_Complex,n)) by POLYNOM5:def 10; :: thesis: verum