theorem Th25: :: E_TRANS1:25

for N0 being Nat
for L being comRing
for F being FinSequence of the carrier of (Polynom-Ring L)
for x being Element of L st len F = N0 + 1 holds
eval (F,x) = (eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*>