theorem Th9: :: RING_EMB:9

for A, B being Ring
for f being Function of A,B st f is monomorphism & ([#] B) \ (rng f) <> {} holds
ex C being Ring 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 Subring of C & G is RingIsomorphism & id A = G * f )