theorem Th22: :: RING_EMB:22

for R being non degenerated comRing
for p0 being Element of (Polynom-Ring (0,R)) holds p0 is not Polynomial of (Polynom-Ring (0,R))