theorem Th31: :: POLYNOM5:31

for L being non empty right_complementable add-associative right_zeroed right-distributive unital doubleLoopStr
for p being Polynomial of L holds eval (p,(0. L)) = p . 0