theorem :: RING_EMB:26

for R being non degenerated comRing holds ([#] (Polynom-Ring (0,R))) /\ ([#] (Polynom-Ring (Polynom-Ring (0,R)))) = {}