let G be Group; :: thesis: for H being strict Group st G,H are_isomorphic & G is commutative holds
H is commutative
let H be strict 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, Def15;
A4: h is onto by A3;

now

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

end;

hence H is commutative by GROUP_1:def 16; :: thesis: verum