theorem Th18: :: POLYNOM9:18

for x being object
for n being Ordinal
for L being non trivial well-unital doubleLoopStr
for b being bag of n
for f being Function of n,L
for u being Element of L st b . x = 0 holds
eval (b,(f +* (x,u))) = eval (b,f)