theorem Th2: :: ALGGEO_1:2

for n being Ordinal
for L being non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g being Element of (Polynom-Ring (n,L))
for x being Function of n,L holds E_eval ((f + g),x) = (E_eval (f,x)) + (E_eval (g,x))