let m be Nat; 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; 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; 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; (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 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))) . u9let u9 be
object ;
( u9 in dom ((DFT (p,x,m)) * (DFT (q,x,m))) implies (DFT ((p *' q),x,m)) . b1 = ((DFT (p,x,m)) * (DFT (q,x,m))) . b1 )assume
u9 in dom ((DFT (p,x,m)) * (DFT (q,x,m)))
;
(DFT ((p *' q),x,m)) . b1 = ((DFT (p,x,m)) * (DFT (q,x,m))) . b1then reconsider u =
u9 as
Element of
NAT by FUNCT_2:def 1;
per cases
( u < m or m <= u )
;
suppose A2:
u < m
;
(DFT ((p *' q),x,m)) . b1 = ((DFT (p,x,m)) * (DFT (q,x,m))) . b1hence (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
;
verum end; suppose A3:
m <= u
;
((DFT (p,x,m)) * (DFT (q,x,m))) . b1 = (DFT ((p *' q),x,m)) . b1thus ((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
;
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; verum