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

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