:: deftheorem Def2 defines E_eval ALGGEO_1:def 2 :
for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for F being FinSequence of the carrier of (Polynom-Ring (n,L))
for x being Function of n,L
for b₅ being FinSequence of the carrier of L holds
( b₅ = E_eval (F,x) iff ( dom b₅ = dom F & ( for i being Nat st i in dom F holds
b₅ . i = E_eval ((F /. i),x) ) ) );