for R being Ring
for p being Element of the carrier of (Polynom-Ring R) holds
( p is constant iff ex a being Element of R st p = a | R )