let G be finite Group; :: thesis: ( G is cyclic iff ex a being Element of G st
for b being Element of G ex n being Nat st b = a |^ n )
thus ( G is cyclic implies ex a being Element of G st
for b being Element of G ex n being Nat st b = a |^ n ) :: thesis: ( ex a being Element of G st
for b being Element of G ex n being Nat st b = a |^ n implies G is cyclic )

proof

assume G is cyclic ; :: thesis: ex a being Element of G st
for b being Element of G ex n being Nat st b = a |^ n
then consider a being Element of G such that
A1: for b being Element of G ex j2 being Integer st b = a |^ j2 by Th17;
take a ; :: thesis: for b being Element of G ex n being Nat st b = a |^ n
let b be Element of G; :: thesis: ex n being Nat st b = a |^ n
consider j2 being Integer such that
A2: b = a |^ j2 by A1;
consider n being Nat such that
A3: ( j2 = n or j2 = - n ) by INT_1:2;

per cases ( j2 = n or j2 = - n ) by A3;

suppose j2 = n ; :: thesis: ex n being Nat st b = a |^ n

hence ex n being Nat st b = a |^ n by A2; :: thesis: verum

end;

suppose A4: j2 = - n ; :: thesis: ex n being Nat st b = a |^ n

n mod (card G) <= card G by NAT_D:1;
then reconsider q9 = (card G) - (n mod (card G)) as Element of NAT by INT_1:5;
take q9 ; :: thesis: b = a |^ q9
b = (a |^ n) " by A2, A4, GROUP_1:36
.= a |^ q9 by Th10 ;
hence b = a |^ q9 ; :: thesis: verum

end;

end;

end;

given a being Element of G such that A5: for b being Element of G ex n being Nat st b = a |^ n ; :: thesis: G is cyclic
for b being Element of G ex j2 being Integer st b = a |^ j2

proof

let b be Element of G; :: thesis: ex j2 being Integer st b = a |^ j2
consider n being Nat such that
A6: b = a |^ n by A5;
reconsider n = n as Integer ;
take n ; :: thesis: b = a |^ n
thus b = a |^ n by A6; :: thesis: verum

end;

hence G is cyclic by Th17; :: thesis: verum