theorem Th25: :: UNIROOTS:25

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