theorem Th26: :: E_TRANS1:26

for L being comRing
for F being FinSequence of the carrier of (Polynom-Ring L)
for x being Element of L holds eval ((~ (Sum F)),x) = Sum (eval (F,x))