for L being Field
for p being Polynomial of L
for m being Element of NAT st m > 0 & len p <= m holds
for x being Element of L
for i being Element of NAT st i < m holds
(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)