theorem :: POLYNOM5:46

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