theorem :: RING_EMB:23

for R being non degenerated comRing holds Polynom-Ring (Polynom-Ring (0,R)), Polynom-Ring (1,R) are_isomorphic