let G be Group; :: thesis: ( G is cyclic implies G is commutative )
assume A1: G is cyclic ; :: thesis: G is commutative
for a, b being Element of G holds a * b = b * a

proof

let a, b be Element of G; :: thesis: a * b = b * a
ex e being Element of G ex j2 being Integer st
( a = e |^ j2 & ex j3 being Integer st b = e |^ j3 )

proof

consider e being Element of G such that
A2: for d being Element of G ex j3 being Integer st d = e |^ j3 by A1, Th17;
take e ; :: thesis: ex j2 being Integer st
( a = e |^ j2 & ex j3 being Integer st b = e |^ j3 )
( ex j2 being Integer st a = e |^ j2 & ex j3 being Integer st b = e |^ j3 ) by A2;
hence ex j2 being Integer st
( a = e |^ j2 & ex j3 being Integer st b = e |^ j3 ) ; :: thesis: verum

end;

then consider e being Element of G, j2, j3 being Integer such that
A3: ( a = e |^ j2 & b = e |^ j3 ) ;
a * b = e |^ (j3 + j2) by A3, GROUP_1:33
.= b * a by A3, GROUP_1:33 ;
hence a * b = b * a ; :: thesis: verum

end;

hence G is commutative ; :: thesis: verum