let L be Field; :: thesis:
let p be Polynomial of L; :: thesis:
let m be Element of NAT ; :: thesis:
assume that
A1: m > 0 and
A2: len p <= m ; :: thesis:
let x be Element of L; :: thesis:
set v = VM (x,m);
for i being Element of NAT st i < m holds
(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)

A3: for k being Nat st k < m holds
(Col ((mConv (p,m)),1)) . (k + 1) = p . k

let k be Nat; :: thesis:
assume A4: k < m ; :: thesis:
then ( 1 <= k + 1 & k + 1 <= m ) by NAT_1:11, NAT_1:13;
then A5: k + 1 in Seg m ;
len (mConv (p,m)) = m by A1, Th28;
then k + 1 in dom (mConv (p,m)) by A5, FINSEQ_1:def 3;
then (Col ((mConv (p,m)),1)) . (k + 1) = (mConv (p,m)) * ((k + 1),1) by MATRIX_0:def 8;
hence (Col ((mConv (p,m)),1)) . (k + 1) = p . k by A4, Th28; :: thesis:

end;

A6: width (VM (x,m)) = m by MATRIX_0:24
.= len (mConv (p,m)) by A1, Th28 ;
then A7: len ((VM (x,m)) * (mConv (p,m))) = len (VM (x,m)) by MATRIX_3:def 4
.= m by MATRIX_0:24 ;
width ((VM (x,m)) * (mConv (p,m))) = width (mConv (p,m)) by A6, MATRIX_3:def 4
.= 1 by A1, Th28 ;
then (VM (x,m)) * (mConv (p,m)) is Matrix of m,1,L by A1, A7, MATRIX_0:20;
then A8: Indices ((VM (x,m)) * (mConv (p,m))) = [:(Seg m),(Seg (width ((VM (x,m)) * (mConv (p,m))))):] by MATRIX_0:25;
A9: len (mConv (p,m)) = m by A1, Th28
.= width (VM (x,m)) by MATRIX_0:24 ;
width ((VM (x,m)) * (mConv (p,m))) = width (mConv (p,m)) by A6, MATRIX_3:def 4
.= 1 by A1, Th28 ;
then A10: 1 in Seg (width ((VM (x,m)) * (mConv (p,m)))) ;
let i be Element of NAT ; :: thesis:
assume A11: i < m ; :: thesis:
A12: for k being Nat st k < m holds
(Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1))

proof

let k be Nat; :: thesis:
assume k < m ; :: thesis:
then ( 1 <= k + 1 & k + 1 <= m ) by NAT_1:11, NAT_1:13;
then k + 1 in Seg m ;
then k + 1 in Seg (width (VM (x,m))) by MATRIX_0:24;
hence (Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1)) by MATRIX_0:def 7; :: thesis:

end;

A13: for k being Nat st k < m holds
(Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k))

proof

let k be Nat; :: thesis:
assume A14: k < m ; :: thesis:
then A15: ( 1 <= k + 1 & k + 1 <= m ) by NAT_1:11, NAT_1:13;
A16: ( 1 <= i + 1 & i + 1 <= m ) by A11, NAT_1:11, NAT_1:13;
(Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1)) by A12, A14
.= pow (x,(((i + 1) - 1) * ((k + 1) - 1))) by A16, A15, Def7
.= pow (x,(i * k)) ;
hence (Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k)) ; :: thesis:

end;

A17: for k being Nat
for a, b, c being Element of L st a = (Line ((VM (x,m)),(i + 1))) . (k + 1) & b = (Col ((mConv (p,m)),1)) . (k + 1) & c = p . k & k < m holds
a * b = (pow (x,(i * k))) * c

proof

let k be Nat; :: thesis:
let a, b, c be Element of L; :: thesis:
assume that
A18: a = (Line ((VM (x,m)),(i + 1))) . (k + 1) and
A19: ( b = (Col ((mConv (p,m)),1)) . (k + 1) & c = p . k ) and
A20: k < m ; :: thesis:
a = pow (x,(i * k)) by A13, A18, A20;
hence a * b = (pow (x,(i * k))) * c by A3, A19, A20; :: thesis:

end;

A21: for k being Element of NAT st 1 <= k & k <= m holds
(mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1)))

proof

A22: len (mConv (p,m)) = m by A1, Th28;
let k be Element of NAT ; :: thesis:
assume that
A23: 1 <= k and
A24: k <= m ; :: thesis:
k in Seg m by A23, A24;
then k in dom (mConv (p,m)) by A22, FINSEQ_1:def 3;
then A25: (Col ((mConv (p,m)),1)) . k = (mConv (p,m)) * (k,1) by MATRIX_0:def 8;
0 < k by A23;
then ( dom p = NAT & k - 1 is Element of NAT ) by FUNCT_2:def 1, NAT_1:20;
then A26: p . (k - 1) = p /. (k - 1) by PARTFUN1:def 6;
Seg (width (VM (x,m))) = Seg m by MATRIX_0:24;
then k in Seg (width (VM (x,m))) by A23, A24;
then (Line ((VM (x,m)),(i + 1))) . k = (VM (x,m)) * ((i + 1),k) by MATRIX_0:def 7;
then reconsider a = (Line ((VM (x,m)),(i + 1))) . k, b = (Col ((mConv (p,m)),1)) . k, c = p . (k - 1) as Element of L by A25, A26;
len (Line ((VM (x,m)),(i + 1))) = width (VM (x,m)) by MATRIX_0:def 7
.= m by MATRIX_0:24
.= len (mConv (p,m)) by A1, Th28
.= len (Col ((mConv (p,m)),1)) by MATRIX_0:def 8 ;
then len (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = len (Line ((VM (x,m)),(i + 1))) by MATRIX_3:6
.= width (VM (x,m)) by MATRIX_0:def 7
.= m by MATRIX_0:24 ;
then dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = Seg m by FINSEQ_1:def 3;
then k in dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) by A23, A24;
then A27: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = a * b by FVSUM_1:60;
A28: a * b = (pow (x,(i * (k - 1)))) * c

proof

A29: 0 < k by A23;
then A30: k - 1 is Nat by NAT_1:20;
( k - 1 <= m - 1 & m - 1 is Nat ) by A1, A24, NAT_1:20, XREAL_1:9;
then A31: k - 1 < (m - 1) + 1 by A30, NAT_1:13;
reconsider l = k - 1 as Nat by A29, NAT_1:20;
a = (Line ((VM (x,m)),(i + 1))) . (l + 1) ;
hence a * b = (pow (x,(i * (k - 1)))) * c by A17, A31; :: thesis:

end;

reconsider d = pow (x,(i * (k - 1))) as Element of L ;
A32: k - 1 >= 0 by A23, NAT_1:20;
d = pow ((x |^ i),(k - 1)) by A23, Th27
.= (power L) . ((x |^ i),(k - 1)) by A32, Def2
.= (power L) . ((x |^ i),(k -' 1)) by A32, XREAL_0:def 2 ;
hence (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) by A28, A27, A32, XREAL_0:def 2; :: thesis:

end;

A33: Sum (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = eval (p,(x |^ i))

proof

A34: for k being Nat st len p < k & k <= m holds
(mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L

proof

A35: 1 <= 1 + (len p) by NAT_1:11;
let k be Nat; :: thesis:
assume that
A36: len p < k and
A37: k <= m ; :: thesis:
A38: len p < (k - 1) + 1 by A36;
(len p) + 1 <= k by A36, NAT_1:13;
then A39: 1 <= k by A35, XXREAL_0:2;
then 1 - 1 <= k - 1 by XREAL_1:9;
then k -' 1 = k - 1 by XREAL_0:def 2;
then A40: k -' 1 >= len p by A38, NAT_1:13;
k in NAT by ORDINAL1:def 12;
then (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) by A21, A37, A39
.= (0. L) * ((power L) . ((x |^ i),(k -' 1))) by A40, ALGSEQ_1:8
.= 0. L ;
hence (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L ; :: thesis:

end;

len (Line ((VM (x,m)),(i + 1))) = width (VM (x,m)) by MATRIX_0:def 7
.= m by MATRIX_0:24
.= len (mConv (p,m)) by A1, Th28
.= len (Col ((mConv (p,m)),1)) by MATRIX_0:def 8 ;
then A41: len (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = len (Line ((VM (x,m)),(i + 1))) by MATRIX_3:6
.= width (VM (x,m)) by MATRIX_0:def 7
.= m by MATRIX_0:24 ;
(len p) - (len p) <= m - (len p) by A2, XREAL_1:9;
then reconsider lengthG = m - (len p) as Element of NAT by INT_1:3;
consider F being FinSequence of L such that
A42: eval (p,(x |^ i)) = Sum F and
A43: len F = len p and
A44: for k being Element of NAT st k in dom F holds
F . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) by POLYNOM4:def 2;
ex G being FinSequence of L st
( dom G = Seg lengthG & ( for k being Nat st k in Seg lengthG holds
G . k = 0. L ) )

proof

defpred S₁[ set , set ] means $2 = 0. L;
A45: for n being Nat st n in Seg lengthG holds
ex x being Element of L st S₁[n,x] ;
ex G being FinSequence of L st
( dom G = Seg lengthG & ( for nn being Nat st nn in Seg lengthG holds
S₁[nn,G . nn] ) ) from FINSEQ_1:sch 5(A45);
hence ex G being FinSequence of L st
( dom G = Seg lengthG & ( for k being Nat st k in Seg lengthG holds
G . k = 0. L ) ) ; :: thesis:

end;

then consider G being FinSequence of L such that
A46: dom G = Seg lengthG and
A47: for k being Nat st k in Seg lengthG holds
G . k = 0. L ;
A48: for k being Element of NAT st k in Seg lengthG holds
G . k = 0. L by A47;
A49: len G = m - (len p) by A46, FINSEQ_1:def 3;
then (len F) + (len G) = m by A43;
then dom (F ^ G) = Seg m by FINSEQ_1:def 7;
then A50: dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = dom (F ^ G) by A41, FINSEQ_1:def 3;
A51: for k being Element of NAT st 1 <= k & k <= len p holds
F . k = (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k

proof

let k be Element of NAT ; :: thesis:
assume that
A52: 1 <= k and
A53: k <= len p ; :: thesis:
A54: k <= m by A2, A53, XXREAL_0:2;
dom F = Seg (len p) by A43, FINSEQ_1:def 3;
then k in dom F by A52, A53;
then F . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) by A44
.= (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k by A21, A52, A54 ;
hence F . k = (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k ; :: thesis:

end;

for k being Nat st k in dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) holds
(mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k

proof

let k be Nat; :: thesis:
(len F) + (len G) = m by A43, A49;
then A55: dom (F ^ G) = Seg m by FINSEQ_1:def 7;
assume A56: k in dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) ; :: thesis:

per cases by A50, A56, A55, FINSEQ_1:1;

suppose A57: ( 1 <= k & k <= len F ) ; :: thesis:

then k in dom F by FINSEQ_3:25;
then (F ^ G) . k = F . k by FINSEQ_1:def 7
.= (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k by A43, A51, A56, A57 ;
hence (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k ; :: thesis:

end;

suppose A58: ( len F < k & k <= m ) ; :: thesis:

then (len F) + 1 <= k by NAT_1:13;
then ((len F) + 1) - (len F) <= k - (len F) by XREAL_1:9;
then reconsider l = k - (len F) as Element of NAT by INT_1:3;
(len p) - m <= m - m by A2, XREAL_1:9;
then - ((len p) - m) >= 0 ;
then reconsider lengthG = m - (len p) as Element of NAT by INT_1:3;
(len F) + 1 <= k by A58, NAT_1:13;
then A59: ((len F) + 1) - (len F) <= k - (len F) by XREAL_1:9;
l <= lengthG by A43, A58, XREAL_1:9;
then A60: l in dom G by A46, A59;
(len F) + (len G) = m by A43, A49;
then dom (F ^ G) = Seg m by FINSEQ_1:def 7;
then len (F ^ G) = m by FINSEQ_1:def 3;
then (F ^ G) . k = G . (k - (len F)) by A58, FINSEQ_1:24
.= 0. L by A46, A47, A60
.= (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k by A43, A34, A58 ;
hence (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k ; :: thesis:

end;

then mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1))) = F ^ G by A50, FINSEQ_1:13;
then Sum (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = (Sum F) + (Sum G) by RLVECT_1:41
.= (Sum F) + (0. L) by A46, A48, POLYNOM3:1
.= eval (p,(x |^ i)) by A42, RLVECT_1:def 4 ;
hence Sum (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = eval (p,(x |^ i)) ; :: thesis:

end;

A61: (Line ((VM (x,m)),(i + 1))) "*" (Col ((mConv (p,m)),1)) = Sum (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) by FVSUM_1:def 9;
( 1 <= i + 1 & i + 1 <= m ) by A11, NAT_1:11, NAT_1:13;
then i + 1 in Seg m ;
then [(i + 1),1] in Indices ((VM (x,m)) * (mConv (p,m))) by A8, A10, ZFMISC_1:def 2;
then ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) = eval (p,(x |^ i)) by A9, A61, A33, MATRIX_3:def 4;
hence (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) by A11, Def6; :: thesis:

end;

hence for i being Element of NAT st i < m holds
(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) ; :: thesis: