theorem LX: :: RING_4:15

for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for p being Element of the carrier of (Polynom-Ring L) holds
( ( not p is zero & p is constant ) iff deg p = 0 )