let m be Nat; :: thesis: 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
let L be Field; :: thesis: 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
let p, q be Polynomial of L; :: thesis: for x being Element of L holds (DFT p,x,m) * (DFT q,x,m) = DFT (p *' q),x,m
let x be Element of L; :: thesis: (DFT p,x,m) * (DFT q,x,m) = DFT (p *' q),x,m
set ep = DFT p,x,m;
set eq = DFT q,x,m;
set epq = DFT (p *' q),x,m;

A1: now

let u9 be set ; :: thesis: ( u9 in dom ((DFT p,x,m) * (DFT q,x,m)) implies (DFT (p *' q),x,m) . b₁ = ((DFT p,x,m) * (DFT q,x,m)) . b₁ )
assume u9 in dom ((DFT p,x,m) * (DFT q,x,m)) ; :: thesis: (DFT (p *' q),x,m) . b₁ = ((DFT p,x,m) * (DFT q,x,m)) . b₁
then reconsider u = u9 as Element of NAT by FUNCT_2:def 1;

per cases ( u < m or m <= u ) ;

suppose A2: u < m ; :: thesis: (DFT (p *' q),x,m) . b₁ = ((DFT p,x,m) * (DFT q,x,m)) . b₁

hence (DFT (p *' q),x,m) . u9 = eval (p *' q),(x |^ u) by Def7
.= (eval p,(x |^ u)) * (eval q,(x |^ u)) by POLYNOM4:27
.= ((DFT p,x,m) . u) * (eval q,(x |^ u)) by A2, Def7
.= ((DFT p,x,m) . u) * ((DFT q,x,m) . u) by A2, Def7
.= ((DFT p,x,m) * (DFT q,x,m)) . u9 by Def2 ;
:: thesis: verum

end;

suppose A3: m <= u ; :: thesis: ((DFT p,x,m) * (DFT q,x,m)) . b₁ = (DFT (p *' q),x,m) . b₁

thus ((DFT p,x,m) * (DFT q,x,m)) . u9 = ((DFT p,x,m) . u) * ((DFT q,x,m) . u) by Def2
.= (0. L) * ((DFT q,x,m) . u) by A3, Def7
.= 0. L by VECTSP_1:36
.= (DFT (p *' q),x,m) . u9 by A3, Def7 ; :: thesis: verum

end;

end;

end;

dom ((DFT p,x,m) * (DFT q,x,m)) = NAT by FUNCT_2:def 1
.= dom (DFT (p *' q),x,m) by FUNCT_2:def 1 ;
hence (DFT p,x,m) * (DFT q,x,m) = DFT (p *' q),x,m by A1, FUNCT_1:9; :: thesis: verum