theorem Th9: :: GROUP_8:9

for G being strict Group
for a being Element of G
for m being Integer holds a |^ (m * (ord a)) = 1_ G