theorem Th13: :: HILB10_2:13

for n being Nat
for b being bag of n
for L being non trivial well-unital doubleLoopStr
for x being Function of n,L
for y being Function of (n + 1),L st y | n = x holds
eval (b,x) = eval ((b bag_extend 0),y)