theorem :: POLYNOM5:37

for L being non empty right_complementable add-associative right_zeroed unital doubleLoopStr
for z0, x being Element of L holds eval (<%z0%>,x) = z0