for G being Group
for a being Element of G
for i being Integer st not a is being_of_order_0 holds
ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i )