theorem Th36: :: NIVEN:38

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