:: deftheorem defconst defines constant RING_4:def 4 :
for R being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for x being Element of the carrier of (Polynom-Ring R) holds
( x is constant iff deg x <= 0 );