theorem Th20: :: HILB10_2:20

for O being Ordinal
for L being non trivial associative commutative well-unital doubleLoopStr
for x being Function of O,L
for b being bag of O
for perm being Permutation of O holds eval (b,x) = eval ((b * perm),(x * perm))