for k, n being Element of NAT
for G being finite strict Group
for a being Element of G st G = gr {a} & card G = n holds
( G = gr {(a |^ k)} iff k gcd n = 1 )