for G being strict Group
for a being Element of G st not a is being_of_order_0 holds
for m being Integer holds a |^ m = a |^ (m mod (ord a))