for n being non zero Element of NAT holds card (n -roots_of_1) = n