theorem Th25: :: RING_EMB:25

for R being non degenerated Ring ex PR being non degenerated Ring ex X being set ex h being Function ex G being Function of (Polynom-Ring R),PR st
( R is Subring of PR & G is RingIsomorphism & id R = G * (canHom R) & X /\ ([#] R) = {} & h is one-to-one & dom h = ([#] (Polynom-Ring R)) \ (rng (canHom R)) & rng h = X & [#] PR = X \/ ([#] R) )