for n being non zero Element of NAT
for x being Element of (MultGroup F_Complex) holds
( ord x divides n iff x in n -roots_of_1 )