card (n -roots_of_1) = n by Th27;
hence n -roots_of_1 is finite ; :: thesis: verum