let n be Nat; :: thesis: for G being finite Group
for a being Element of G holds (a |^ n) " = a |^ ((card G) - (n mod (card G)))
let G be finite Group; :: thesis: for a being Element of G holds (a |^ n) " = a |^ ((card G) - (n mod (card G)))
let a be Element of G; :: thesis: (a |^ n) " = a |^ ((card G) - (n mod (card G)))
set q = card G;
set p9 = n mod (card G);
n mod (card G) <= card G by NAT_D:1;
then reconsider q9 = (card G) - (n mod (card G)) as Element of NAT by INT_1:5;
(a |^ n) * (a |^ ((card G) - (n mod (card G)))) = a |^ (n + q9) by GROUP_1:33
.= a |^ ((((card G) * (n div (card G))) + (n mod (card G))) + q9) by NAT_D:2
.= a |^ ((((card G) * (n div (card G))) + (card G)) + ((- (n mod (card G))) + (n mod (card G))))
.= (a |^ (((card G) * (n div (card G))) + (card G))) * (a |^ ((- (n mod (card G))) + (n mod (card G)))) by GROUP_1:33
.= (a |^ (((card G) * (n div (card G))) + (card G))) * ((a |^ (- (n mod (card G)))) * (a |^ (n mod (card G)))) by GROUP_1:33
.= (a |^ (((card G) * (n div (card G))) + (card G))) * (((a |^ (n mod (card G))) ") * (a |^ (n mod (card G)))) by GROUP_1:36
.= (a |^ (((card G) * (n div (card G))) + (card G))) * (1_ G) by GROUP_1:def 5
.= a |^ ((card G) * ((n div (card G)) + 1)) by GROUP_1:def 4
.= (a |^ (card G)) |^ ((n div (card G)) + 1) by GROUP_1:35
.= (1_ G) |^ ((n div (card G)) + 1) by Th9
.= 1_ G by GROUP_1:31 ;
hence (a |^ n) " = a |^ ((card G) - (n mod (card G))) by GROUP_1:12; :: thesis: verum