let G, H 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 12 :: thesis: h1 * h2 = h2 * h1
reconsider c = h1, d = h2 as Element of H by GROUP_2:42;
h1 in Image g ;
then consider a being Element of G such that
A2: h1 = g . a by Th45;
h2 in Image g ;
then consider b being Element of G such that
A3: h2 = g . b by Th45;
thus h1 * h2 = c * d by GROUP_2:43
.= g . (a * b) by A2, A3, Def6
.= g . (b * a) by A1, Lm2
.= d * c by A2, A3, Def6
.= h2 * h1 by GROUP_2:43 ; :: thesis: verum