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);

.= 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

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

dom ((DFT (p,x,m)) * (DFT (q,x,m))) =
NAT
by FUNCT_2:def 1
(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_{1} = ((DFT (p,x,m)) * (DFT (q,x,m))) . b_{1} )

assume u9 in dom ((DFT (p,x,m)) * (DFT (q,x,m))) ; :: thesis: (DFT ((p *' q),x,m)) . b_{1} = ((DFT (p,x,m)) * (DFT (q,x,m))) . b_{1}

then reconsider u = u9 as Element of NAT by FUNCT_2:def 1;

end;assume u9 in dom ((DFT (p,x,m)) * (DFT (q,x,m))) ; :: thesis: (DFT ((p *' q),x,m)) . b

then reconsider u = u9 as Element of NAT by FUNCT_2:def 1;

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

end;

suppose A2:
u < m
; :: thesis: (DFT ((p *' q),x,m)) . b_{1} = ((DFT (p,x,m)) * (DFT (q,x,m))) . b_{1}

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;.= (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

suppose A3:
m <= u
; :: thesis: ((DFT (p,x,m)) * (DFT (q,x,m))) . b_{1} = (DFT ((p *' q),x,m)) . b_{1}

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;.= (0. L) * ((DFT (q,x,m)) . u) by A3, Def6

.= 0. L

.= (DFT ((p *' q),x,m)) . u9 by A3, Def6 ; :: thesis: verum

.= 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