theorem Th11: :: POLYNOM2:19

for n being Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L
for b being bag of n st Support p = {b} holds
for x being Function of n,L holds eval (p,x) = (p . b) * (eval (b,x))