theorem Th21: :: UNIROOTS:21

for n being non zero Element of NAT
for x being Element of F_Complex holds
( x in n -roots_of_1 iff x is CRoot of n, 1_ F_Complex )