theorem Th8: :: POLYNOM2:16

for n being Ordinal
for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for b1, b2 being bag of n
for x being Function of n,L holds eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x))