theorem :: UNIROOTS:33

for n being non zero Element of NAT ex x being Element of (MultGroup F_Complex) st ord x = n