let n be Element of 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 p' = n mod (card G);
n mod (card G) <= card G by NAT_D:1;
then reconsider q' = (card G) - (n mod (card G)) as Element of NAT by INT_1:18;
(a |^ n) * (a |^ ((card G) - (n mod (card G)))) = a |^ (n + q') by GROUP_1:63
.= a |^ ((((card G) * (n div (card G))) + (n mod (card G))) + q') 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:63
.= (a |^ (((card G) * (n div (card G))) + (card G))) * ((a |^ (- (n mod (card G)))) * (a |^ (n mod (card G)))) by GROUP_1:63
.= (a |^ (((card G) * (n div (card G))) + (card G))) * (((a |^ (n mod (card G))) " ) * (a |^ (n mod (card G)))) by GROUP_1:70
.= (a |^ (((card G) * (n div (card G))) + (card G))) * (1_ G) by GROUP_1:def 6
.= a |^ ((card G) * ((n div (card G)) + 1)) by GROUP_1:def 5
.= (a |^ (card G)) |^ ((n div (card G)) + 1) by GROUP_1:67
.= (1_ G) |^ ((n div (card G)) + 1) by Th29
.= 1_ G by GROUP_1:61 ;
hence (a |^ n) " = a |^ ((card G) - (n mod (card G))) by GROUP_1:20; :: thesis: verum