theorem Th45: :: UNIROOTS:45

for n being non zero Element of NAT holds BRoots (unital_poly (F_Complex,n)) = ((n -roots_of_1),1) -bag