:: deftheorem Def1 defines eval POLYNOM2:def 2 :
for n being Ordinal
for b being bag of n
for L being non trivial well-unital doubleLoopStr
for x being Function of n,L
for b₅ being Element of L holds
( b₅ = eval (b,x) iff ex y being FinSequence of the carrier of L st
( len y = len (SgmX ((RelIncl n),(support b))) & b₅ = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) ) );