for k being Element of NAT
for G being finite Group
for a being Element of G st k gcd (ord a) = 1 holds
ord a = ord (a |^ k)