for L being Field
for p, q being Polynomial of L
for m being Element of NAT st m > 0 & len p <= m & len q <= m holds
for x being Element of L st x is_primitive_root_of_degree 2 * m holds
DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q)