let G be finite Group; :: thesis: for a, b being Element of G holds
( b in gr {a} iff ex p being Element of NAT st b = a |^ p )
let a, b be Element of G; :: thesis: ( b in gr {a} iff ex p being Element of NAT st b = a |^ p )
reconsider a0 = a as Element of (gr {a}) by GR_CY_2:2, STRUCT_0:def 5;
X1: gr {a0} = gr {a} by GR_CY_2:3;

hereby :: thesis: ( ex p being Element of NAT st b = a |^ p implies b in gr {a} )

assume b in gr {a} ; :: thesis: ex p being Element of NAT st b = a |^ p
then reconsider b0 = b as Element of (gr {a}) ;
consider p being Element of NAT such that
A1: b0 = a0 |^ p by X1, GR_CY_2:6;
b = a |^ p by GROUP_4:2, A1;
hence ex p being Element of NAT st b = a |^ p ; :: thesis: verum

end;

given p being Element of NAT such that A1: b = a |^ p ; :: thesis: b in gr {a}
b = a0 |^ p by GROUP_4:2, A1;
hence b in gr {a} ; :: thesis: verum