theorem Th6: :: POLYNOM2:14

for n being Ordinal
for L being non trivial well-unital doubleLoopStr
for x being Function of n,L holds eval ((EmptyBag n),x) = 1. L