theorem Th25: :: HILB10_2:25

for O being Ordinal
for L being non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of O,L
for x being Function of O,L
for perm being Permutation of O holds eval (p,x) = eval ((p permuted_by perm),(x * (perm ")))