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

A4: now :: thesis: for u9 being object st u9 in dom (DFT (p,x,m)) holds
(DFT (p,x,m)) . u9 = (aConv ((VM (x,m)) * (mConv (p,m)))) . u9

let u9 be object ; :: 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_0:24
.= 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_0:24 ;
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, Def4 ; :: 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_0:24
.= 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_0:24 ;
thus (DFT (p,x,m)) . u9 = 0. L by A7, Def6
.= (aConv ((VM (x,m)) * (mConv (p,m)))) . u9 by A7, A8, Def4 ; :: 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:2; :: thesis: verum