for n being non zero Element of NAT
for x, y being Element of COMPLEX st x in n -roots_of_1 & y in n -roots_of_1 holds
x * y in n -roots_of_1