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 )

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

( ( 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 A3:
G = gr {b}
; :: thesis: for a being Element of G ex p being Element of NAT st a = b |^ p
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

end;for a being Element of G ex i being Integer st a = b |^ i

proof

hence
G = gr {b}
by Th5; :: thesis: verum
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;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

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