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