theorem :: RING_EMB:27

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 (Polynom-Ring (0,R))),PR st
( Polynom-Ring (0,R) is Subring of PR & G is RingIsomorphism & id (Polynom-Ring (0,R)) = G * (canHom (Polynom-Ring (0,R))) & X /\ ([#] (Polynom-Ring (0,R))) = {} & h is one-to-one & dom h = ([#] (Polynom-Ring (Polynom-Ring (0,R)))) \ (rng (canHom (Polynom-Ring (0,R)))) & rng h = X & [#] PR = X \/ ([#] (Polynom-Ring (0,R))) ) by Th25;