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