:: deftheorem Def1 defines Poly-INT INT_5:def 1 :
for fp being FinSequence of INT
for b₂ being Function of INT,INT holds
( b₂ = Poly-INT fp iff for x being Element of INT ex fr being FinSequence of INT st
( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = (fp . d) * (x |^ (d -' 1)) ) & b₂ . x = Sum fr ) );