theorem GRCY211: :: GROUP_18:7

for k being Element of NAT
for G being finite Group
for a being Element of G holds ord a divides k * (ord (a |^ k))