:: deftheorem Def6 defines DFT POLYNOM8:def 7 :
for m being Nat
for L being non empty well-unital doubleLoopStr
for p being Polynomial of L
for x being Element of L
for b₅ being AlgSequence of L holds
( b₅ = DFT (p,x,m) iff ( ( for i being Nat st i < m holds
b₅ . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
b₅ . i = 0. L ) ) );