theorem Th35: :: POLYNOM9:35

for O being Ordinal
for R being non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for t being bag of O
for p being Polynomial of O,R
for i being object
for x being Function of O,R st i in O holds
eval ((Subst (t,i,p)),x) = eval (t,(x +* (i,(eval (p,x)))))