theorem :: POLYNOM5:45

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