theorem Th37: :: POLYNOM9:37

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