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;

b = a0 |^ p by GROUP_4:2, A1;

hence b in gr {a} ; :: thesis: verum

( 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} )

given p being Element of NAT such that A1:
b = a |^ p
; :: thesis: 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;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

b = a0 |^ p by GROUP_4:2, A1;

hence b in gr {a} ; :: thesis: verum