let G be Group; :: thesis: 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 )
let a be Element of G; :: thesis: 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 )
let i be Integer; :: thesis: ( not a is being_of_order_0 implies ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i ) )
assume A1: not a is being_of_order_0 ; :: thesis: ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i )
ord a <> 0 by A1, GROUP_1:def 12;
then A2: abs i <= (abs i) * (ord a) by NAT_1:14, XREAL_1:153;
0 <= ((abs i) * (ord a)) + i

proof

per cases ( i < 0 or 0 <= i ) ;

suppose i < 0 ; :: thesis: 0 <= ((abs i) * (ord a)) + i

then A3: abs i = - i by ABSVALUE:def 1;
(abs i) + i <= ((abs i) * (ord a)) + i by A2, XREAL_1:8;
hence 0 <= ((abs i) * (ord a)) + i by A3; :: thesis: verum

end;

suppose 0 <= i ; :: thesis: 0 <= ((abs i) * (ord a)) + i

hence 0 <= ((abs i) * (ord a)) + i ; :: thesis: verum

end;

end;

end;

then A4: ((abs i) * (ord a)) + i is Element of NAT by INT_1:16;
a |^ (((abs i) * (ord a)) + i) = (a |^ ((abs i) * (ord a))) * (a |^ i) by GROUP_1:63
.= ((a |^ (ord a)) |^ (abs i)) * (a |^ i) by GROUP_1:67
.= ((1_ G) |^ (abs i)) * (a |^ i) by GROUP_1:82
.= (1_ G) * (a |^ i) by GROUP_1:61
.= a |^ i by GROUP_1:def 5 ;
hence ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i ) by A4; :: thesis: verum