theorem Th14: :: POLYNOM9:14

for i being Nat
for x being object
for n being Ordinal
for L being non trivial well-unital doubleLoopStr
for y being Function of n,L st x in n holds
eval (((EmptyBag n) +* (x,i)),y) = (power L) . ((y . x),i)