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