let L be 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 & emb ((2 * m),L) <> 0. L holds
((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q
let p, q be 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 & emb ((2 * m),L) <> 0. L holds
((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q
let m be Element of NAT ; ( m > 0 & len p <= m & len q <= m implies for x being Element of L st x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L holds
((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q )
assume A1:
( m > 0 & len p <= m & len q <= m )
; for x being Element of L st x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L holds
((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q
let x be Element of L; ( x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L implies ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q )
assume A2:
x is_primitive_root_of_degree 2 * m
; ( not emb ((2 * m),L) <> 0. L or ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q )
assume A3:
emb ((2 * m),L) <> 0. L
; ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q
((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) =
((emb ((2 * m),L)) ") * (DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)))
by Th34
.=
((emb ((2 * m),L)) ") * ((emb ((2 * m),L)) * (p *' q))
by A1, A2, Th43
.=
(((emb ((2 * m),L)) ") * (emb ((2 * m),L))) * (p *' q)
by Th10
.=
(1. L) * (p *' q)
by A3, VECTSP_1:def 10
.=
p *' q
by POLYNOM5:27
;
hence
((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q
; verum