:: deftheorem defeval defines Ext_eval FIELD_11:def 4 :
for R, S being non degenerated comRing
for n being Ordinal
for p being Polynomial of n,R
for x being Function of n,S
for b₆ being Element of S holds
( b₆ = Ext_eval (p,x) iff ex y being FinSequence of S st
( b₆ = Sum y & len y = len (SgmX ((BagOrder n),(Support p))) & ( for i being Element of NAT st 1 <= i & i <= len y holds
y . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) );