theorem Th7: :: POLYNOM2:15

for n being Ordinal
for L being non trivial well-unital doubleLoopStr
for u being set
for b being bag of n st support b = {u} holds
for x being Function of n,L holds eval (b,x) = (power L) . ((x . u),(b . u))