for G being finite commutative Group
for m being Nat
for H being finite Subgroup of G st the carrier of H = { x where x is Element of G : x |^ m = 1_ G } holds
for q being Prime st q in support (prime_factorization (card H)) holds
not q,m are_coprime