let G be finite strict Group; :: thesis: for b being Element of G holds
( ( for a being Element of G ex p being Element of NAT st a = b |^ p ) iff G = gr {b} )
let b be Element of G; :: thesis: ( ( for a being Element of G ex p being Element of NAT st a = b |^ p ) iff G = gr {b} )
thus ( ( for a being Element of G ex p being Element of NAT st a = b |^ p ) implies G = gr {b} ) :: thesis: ( G = gr {b} implies for a being Element of G ex p being Element of NAT st a = b |^ p )

proof

assume A1: for a being Element of G ex p being Element of NAT st a = b |^ p ; :: thesis: G = gr {b}
for a being Element of G ex i being Integer st a = b |^ i

proof

let a be Element of G; :: thesis: ex i being Integer st a = b |^ i
consider p being Element of NAT such that
A2: a = b |^ p by A1;
reconsider p1 = p as Integer ;
take p1 ; :: thesis: a = b |^ p1
thus a = b |^ p1 by A2; :: thesis: verum

end;

hence G = gr {b} by Th11; :: thesis: verum

end;

assume A3: G = gr {b} ; :: thesis: for a being Element of G ex p being Element of NAT st a = b |^ p
let a be Element of G; :: thesis: ex p being Element of NAT st a = b |^ p
consider i being Integer such that
A4: a = b |^ i by A3, Th11;
reconsider n1 = card G as Integer ;
A5: n1 > 0 by GROUP_1:90;
reconsider p = i mod n1 as Element of NAT by INT_1:16, NEWTON:78;
A6: a = b |^ (((i div n1) * n1) + (i mod n1)) by A4, A5, NEWTON:80
.= (b |^ ((i div n1) * n1)) * (b |^ (i mod n1)) by GROUP_1:63
.= ((b |^ (i div n1)) |^ (card G)) * (b |^ (i mod n1)) by GROUP_1:67
.= (1_ G) * (b |^ (i mod n1)) by GR_CY_1:29
.= b |^ (i mod n1) by GROUP_1:def 5 ;
take p ; :: thesis: a = b |^ p
thus a = b |^ p by A6; :: thesis: verum