theorem Th5: :: ALGGEO_1:5

for n being Ordinal
for L being non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for F being FinSequence of the carrier of (Polynom-Ring (n,L))
for x being Function of n,L holds E_eval ((Sum F),x) = Sum (E_eval (F,x))