let k be Element of NAT ; :: thesis: for G being finite Group

for a being Element of G holds

( gr {a} = gr {(a |^ k)} iff k gcd (ord a) = 1 )

let G be finite Group; :: thesis: for a being Element of G holds

( gr {a} = gr {(a |^ k)} iff k gcd (ord a) = 1 )

let a be Element of G; :: thesis: ( gr {a} = gr {(a |^ k)} iff k gcd (ord a) = 1 )

set n = ord a;

reconsider a0 = a as Element of (gr {a}) by GR_CY_2:2, STRUCT_0:def 5;

A11: gr {a0} = gr {a} by GR_CY_2:3;

card (gr {a}) = ord a by GR_CY_1:7;

then ( gr {a} = gr {(a0 |^ k)} iff k gcd (ord a) = 1 ) by A11, GR_CY_2:12;

hence ( gr {a} = gr {(a |^ k)} iff k gcd (ord a) = 1 ) by GROUP_4:2, GR_CY_2:3; :: thesis: verum

for a being Element of G holds

( gr {a} = gr {(a |^ k)} iff k gcd (ord a) = 1 )

let G be finite Group; :: thesis: for a being Element of G holds

( gr {a} = gr {(a |^ k)} iff k gcd (ord a) = 1 )

let a be Element of G; :: thesis: ( gr {a} = gr {(a |^ k)} iff k gcd (ord a) = 1 )

set n = ord a;

reconsider a0 = a as Element of (gr {a}) by GR_CY_2:2, STRUCT_0:def 5;

A11: gr {a0} = gr {a} by GR_CY_2:3;

card (gr {a}) = ord a by GR_CY_1:7;

then ( gr {a} = gr {(a0 |^ k)} iff k gcd (ord a) = 1 ) by A11, GR_CY_2:12;

hence ( gr {a} = gr {(a |^ k)} iff k gcd (ord a) = 1 ) by GROUP_4:2, GR_CY_2:3; :: thesis: verum