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)) )
A1: m in NAT by ORDINAL1:def 13;
assume A2: ( 0 < m & 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: dom (DFT p,x,m) = NAT by FUNCT_2:def 1
.= dom (aConv ((VM x,m) * (mConv p,m))) by FUNCT_2:def 1 ;

now

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

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

suppose A4: 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 A2, Th28 ;
then A5: 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) . u' = ((VM x,m) * (mConv p,m)) * (u + 1),1 by A1, A2, A4, Th41
.= (aConv ((VM x,m) * (mConv p,m))) . u' by A4, A5, Def5 ; :: thesis: verum

end;

suppose A6: 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 A2, Th28 ;
then A7: 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) . u' = 0. L by A6, Def7
.= (aConv ((VM x,m) * (mConv p,m))) . u' by A6, A7, Def5 ; :: thesis: verum

end;

end;

end;

hence DFT p,x,m = aConv ((VM x,m) * (mConv p,m)) by A3, FUNCT_1:9; :: thesis: verum