let n be non empty Element of NAT ; :: thesis: 1_ F_Complex in n -roots_of_1
1_ F_Complex = (power F_Complex ) . (1_ F_Complex ),n by Th10;
then 1_ F_Complex is CRoot of n, 1_ F_Complex by COMPLFLD:def 2;
hence 1_ F_Complex in n -roots_of_1 ; :: thesis: verum