let G, H be Group; :: thesis: ( G,H are_isomorphic & G is commutative implies H is commutative )
assume that
A1: G,H are_isomorphic and
A2: G is commutative ; :: thesis: H is commutative
consider h being Homomorphism of G,H such that
A3: h is bijective by A1;

now :: thesis: for c, d being Element of H holds c * d = d * c

let c, d be Element of H; :: thesis: c * d = d * c
consider a being Element of G such that
A4: h . a = c by A3, Th58;
consider b being Element of G such that
A5: h . b = d by A3, Th58;
thus c * d = h . (a * b) by A4, A5, Def6
.= h . (b * a) by A2
.= d * c by A4, A5, Def6 ; :: thesis: verum

end;

hence H is commutative ; :: thesis: verum