for n being non zero Element of NAT
for x being Element of F_Complex st x in n -roots_of_1 holds
|.x.| = 1