theorem Th25: :: POLYNOM7:25

for n being Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for a being Element of L
for x being Function of n,L holds eval ((a | (n,L)),x) = a