:: deftheorem Def1 defines Ext_eval ALGNUM_1:def 1 :
for A, B being Ring
for p being Polynomial of A
for x, b₅ being Element of B holds
( b₅ = Ext_eval (p,x) iff ex F being FinSequence of B st
( b₅ = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) ) ) );