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} )
reconsider n1 = card G as Integer ;
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 Th5; :: 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, Th5;
reconsider p = i mod n1 as Element of NAT by INT_1:3, NEWTON:64;
take p ; :: thesis: a = b |^ p
a = b |^ (((i div n1) * n1) + (i mod n1)) by A4, NEWTON:66
.= (b |^ ((i div n1) * n1)) * (b |^ (i mod n1)) by GROUP_1:33
.= ((b |^ (i div n1)) |^ (card G)) * (b |^ (i mod n1)) by GROUP_1:35
.= (1_ G) * (b |^ (i mod n1)) by GR_CY_1:9
.= b |^ (i mod n1) by GROUP_1:def 4 ;
hence a = b |^ p ; :: thesis: verum