theorem :: RING_EMB:14

for A, B being AbGroup
for f being Homomorphism of A,B st f is one-to-one & ([#] B) \ (rng f) <> {} holds
ex C being AbGroup ex X being set ex h being Function ex G being Function of B,C st
( X /\ ([#] A) = {} & h is one-to-one & dom h = ([#] B) \ (rng f) & rng h = X & [#] C = X \/ ([#] A) & A is SubAbGr of C & G is Homomorphism of B,C & id A = G * f )