for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of {},L
for x being Function of {},L holds eval (p,x) = p . (EmptyBag {})