theorem Th4: :: ALGGEO_1:4

for N0 being Nat
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 st len F = N0 + 1 holds
E_eval (F,x) = (E_eval ((F | N0),x)) ^ <*(E_eval ((F /. (len F)),x))*>