let G be Group; :: thesis: ( G is cyclic Group iff ex a being Element of G st
for b being Element of G ex j1 being Integer st b = a |^ j1 )
thus ( G is cyclic Group implies ex a being Element of G st
for b being Element of G ex j1 being Integer st b = a |^ j1 ) :: thesis: ( ex a being Element of G st
for b being Element of G ex j1 being Integer st b = a |^ j1 implies G is cyclic Group )
proof
assume G is cyclic Group ; :: thesis: ex a being Element of G st
for b being Element of G ex j1 being Integer st b = a |^ j1
then consider a being Element of G such that
A1: multMagma(# the carrier of G, the multF of G #) = gr {a} by Def7;
take a ; :: thesis: for b being Element of G ex j1 being Integer st b = a |^ j1
for b being Element of G ex j1 being Integer st b = a |^ j1 by A1, Th5, STRUCT_0:def 5;
hence for b being Element of G ex j1 being Integer st b = a |^ j1 ; :: thesis: verum
end;
given a being Element of G such that A2: for b being Element of G ex j1 being Integer st b = a |^ j1 ; :: thesis: G is cyclic Group
for b being Element of G holds b in gr {a}
proof
let b be Element of G; :: thesis: b in gr {a}
ex j1 being Integer st b = a |^ j1 by A2;
hence b in gr {a} by Th5; :: thesis: verum
end;
then multMagma(# the carrier of G, the multF of G #) = gr {a} by GROUP_2:62;
hence G is cyclic Group by Def7; :: thesis: verum