theorem Th53: :: POLYNOM9:53

for X being Ordinal
for S being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of X,S
for i being object
for x being Function of X,S st i in X \ (vars p) holds
for s being Element of S holds eval (p,x) = eval (p,(x +* (i,s)))