theorem Th90: :: RING_4:35

for R being domRing
for a being Element of R holds
( a | R is Unit of (Polynom-Ring R) iff a is Unit of R )