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

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