theorem Th8: :: RATFUNC1:8

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