:: deftheorem Def8 defines eval E_TRANS1:def 7 :
for L being comRing
for F being FinSequence of the carrier of (Polynom-Ring L)
for x being Element of L
for b₄ being FinSequence of the carrier of L holds
( b₄ = eval (F,x) iff ( dom b₄ = dom F & ( for i being Nat st i in dom F holds
b₄ . i = eval ((~ (F /. i)),x) ) ) );