for O being set
for G, H, I being GroupWithOperators of O
for f being Homomorphism of G,H
for g being Homomorphism of H,I holds the carrier of (Ker (g * f)) = f " the carrier of (Ker g)