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

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 ) by A2;
hence ex j2 being Integer st
( a = e |^ j2 & ex j3 being Integer st b = e |^ j3 ) ; :: thesis:

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:

end;