theorem Th30: :: INT_7:30

for G being Group
for z being Element of G
for d, l being Element of NAT st G is finite & ord z = d * l holds
ord (z |^ d) = l