let G be finite Group; :: thesis: for a being Element of G holds a |^ (card G) = 1_ G
let a be Element of G; :: thesis: a |^ (card G) = 1_ G
ord a divides card G by Th28;
then consider t being Nat such that
A1: card G = (ord a) * t by NAT_D:def 3;
a |^ (card G) = (a |^ (ord a)) |^ t by A1, GROUP_1:67
.= (1_ G) |^ t by GROUP_1:82
.= 1_ G by GROUP_1:61 ;
hence a |^ (card G) = 1_ G ; :: thesis: verum