let k be Element of NAT ; :: thesis: for G being finite Group
for a being Element of G st k gcd (ord a) = 1 holds
ord a = ord (a |^ k)
let G be finite Group; :: thesis: for a being Element of G st k gcd (ord a) = 1 holds
ord a = ord (a |^ k)
let a be Element of G; :: thesis: ( k gcd (ord a) = 1 implies ord a = ord (a |^ k) )
assume k gcd (ord a) = 1 ; :: thesis: ord a = ord (a |^ k)
then A1: gr {a} = gr {(a |^ k)} by GRCY212;
card (gr {a}) = ord a by GR_CY_1:7;
hence ord a = ord (a |^ k) by A1, GR_CY_1:7; :: thesis: verum