for G, H being Group
for g being Homomorphism of G,H ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective & g = h * (nat_hom (Ker g)) ) by Lm3;