let G1, G2 be Group; :: thesis: for phi being Homomorphism of G1,G2
for x being Element of G1 st x in commutators G1 holds
phi . x in commutators G2
let phi be Homomorphism of G1,G2; :: thesis: for x being Element of G1 st x in commutators G1 holds
phi . x in commutators G2
let x be Element of G1; :: thesis: ( x in commutators G1 implies phi . x in commutators G2 )
assume x in commutators G1 ; :: thesis: phi . x in commutators G2
then consider a, b being Element of G1 such that
A2: x = [.a,b.] by GROUP_5:58;
phi . x = [.(phi . a),(phi . b).] by A2, GROUP_6:34;
hence phi . x in commutators G2 by GROUP_5:58; :: thesis: verum