let R be non degenerated Ring; :: thesis: 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) )
consider PR being Ring, X being set , h being Function, G being Function of (Polynom-Ring R),PR such that
A1: ( X /\ ([#] R) = {} & h is one-to-one & dom h = ([#] (Polynom-Ring R)) \ (rng (canHom R)) & rng h = X & [#] PR = X \/ ([#] R) & R is Subring of PR & G is RingIsomorphism & id R = G * (canHom R) ) by Th24, Th9;
A2: ( 1. PR = 1. R & 0. PR = 0. R ) by A1, C0SP1:def 3;
PR is non degenerated Ring by A2, STRUCT_0:def 8;
hence 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) ) by A1; :: thesis: verum