for m being Nat
for L being Field
for p, q being Polynomial of L
for x being Element of L holds (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m)