let G be strict Group; :: thesis: 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))
let a be Element of G; :: thesis: ( not a is being_of_order_0 implies for m being Integer holds a |^ m = a |^ (m mod (ord a)) )
assume A1: not a is being_of_order_0 ; :: thesis: for m being Integer holds a |^ m = a |^ (m mod (ord a))
let m be Integer; :: thesis: a |^ m = a |^ (m mod (ord a))
ord a <> 0 by A1, GROUP_1:def 11;
then m mod (ord a) = m - ((m div (ord a)) * (ord a)) by INT_1:def 10;
then a |^ (m mod (ord a)) = a |^ (m + (- ((1 * (m div (ord a))) * (ord a))))
.= (a |^ m) * (a |^ ((- (m div (ord a))) * (ord a))) by GROUP_1:33
.= (a |^ m) * (1_ G) by Th9
.= a |^ m by GROUP_1:def 4 ;
hence a |^ m = a |^ (m mod (ord a)) ; :: thesis: verum