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 :: thesis: for u9 being object st u9 in dom ((DFT (p,x,m)) * (DFT (q,x,m))) holds
(DFT ((p *' q),x,m)) . u9 = ((DFT (p,x,m)) * (DFT (q,x,m))) . u9

let u9 be object ; :: 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 Def6
.= (eval (p,(x |^ u))) * (eval (q,(x |^ u))) by POLYNOM4:24
.= ((DFT (p,x,m)) . u) * (eval (q,(x |^ u))) by A2, Def6
.= ((DFT (p,x,m)) . u) * ((DFT (q,x,m)) . u) by A2, Def6
.= ((DFT (p,x,m)) * (DFT (q,x,m))) . u9 by LOPBAN_3:def 7 ;
:: 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 LOPBAN_3:def 7
.= (0. L) * ((DFT (q,x,m)) . u) by A3, Def6
.= 0. L
.= (DFT ((p *' q),x,m)) . u9 by A3, Def6 ; :: 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:2; :: thesis: verum