let n be non zero Element of NAT ; :: thesis: 1_ F_Complex in n -roots_of_1
1_ F_Complex = (power F_Complex) . ((1_ F_Complex),n) by Th8;
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