theorem Th3: :: ALGGEO_1:3

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, 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))