let H, G be Group; :: thesis: for g being Homomorphism of G,H st G is commutative Group holds
Image g is commutative
let g be Homomorphism of G,H; :: thesis: ( G is commutative Group implies Image g is commutative )
assume A1: G is commutative Group ; :: thesis: Image g is commutative
let h1, h2 be Element of (Image g); :: according to GROUP_1:def 16 :: thesis: h1 * h2 = h2 * h1
reconsider c = h1, d = h2 as Element of H by GROUP_2:51;
h1 in Image g by STRUCT_0:def 5;
then consider a being Element of G such that
A2: h1 = g . a by Th54;
h2 in Image g by STRUCT_0:def 5;
then consider b being Element of G such that
A3: h2 = g . b by Th54;
thus h1 * h2 = c * d by GROUP_2:52
.= g . (a * b) by A2, A3, Def7
.= g . (b * a) by A1, Lm2
.= d * c by A2, A3, Def7
.= h2 * h1 by GROUP_2:52 ; :: thesis: verum