let L be Field; :: thesis: for p being Polynomial of L
for m being Nat st 0 < m & len p <= m holds
for x being Element of L holds DFT p,x,m = aConv ((VM x,m) * (mConv p,m))
let p be Polynomial of L; :: thesis: for m being Nat st 0 < m & len p <= m holds
for x being Element of L holds DFT p,x,m = aConv ((VM x,m) * (mConv p,m))
let m be Nat; :: thesis: ( 0 < m & len p <= m implies for x being Element of L holds DFT p,x,m = aConv ((VM x,m) * (mConv p,m)) )
assume that
A1: 0 < m and
A2: len p <= m ; :: thesis: for x being Element of L holds DFT p,x,m = aConv ((VM x,m) * (mConv p,m))
let x be Element of L; :: thesis: DFT p,x,m = aConv ((VM x,m) * (mConv p,m))
A3: m in NAT by ORDINAL1:def 13;

A4: now

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

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

suppose A5: u < m ; :: thesis: (DFT p,x,m) . b₁ = (aConv ((VM x,m) * (mConv p,m))) . b₁

width (VM x,m) = m by MATRIX_1:25
.= len (mConv p,m) by A1, Th28 ;
then A6: len ((VM x,m) * (mConv p,m)) = len (VM x,m) by MATRIX_3:def 4
.= m by MATRIX_1:25 ;
thus (DFT p,x,m) . u9 = ((VM x,m) * (mConv p,m)) * (u + 1),1 by A3, A2, A5, Th41
.= (aConv ((VM x,m) * (mConv p,m))) . u9 by A5, A6, Def5 ; :: thesis: verum

end;

suppose A7: m <= u ; :: thesis: (DFT p,x,m) . b₁ = (aConv ((VM x,m) * (mConv p,m))) . b₁

width (VM x,m) = m by MATRIX_1:25
.= len (mConv p,m) by A1, Th28 ;
then A8: len ((VM x,m) * (mConv p,m)) = len (VM x,m) by MATRIX_3:def 4
.= m by MATRIX_1:25 ;
thus (DFT p,x,m) . u9 = 0. L by A7, Def7
.= (aConv ((VM x,m) * (mConv p,m))) . u9 by A7, A8, Def5 ; :: thesis: verum

end;

end;

end;

dom (DFT p,x,m) = NAT by FUNCT_2:def 1
.= dom (aConv ((VM x,m) * (mConv p,m))) by FUNCT_2:def 1 ;
hence DFT p,x,m = aConv ((VM x,m) * (mConv p,m)) by A4, FUNCT_1:9; :: thesis: verum