let L be Field; :: thesis: for p being Polynomial of L

for m being Element of NAT st m > 0 & len p <= m holds

for x being Element of L

for i being Element of NAT st i < m holds

(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)

let p be Polynomial of L; :: thesis: for m being Element of NAT st m > 0 & len p <= m holds

for x being Element of L

for i being Element of NAT st i < m holds

(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)

let m be Element of NAT ; :: thesis: ( m > 0 & len p <= m implies for x being Element of L

for i being Element of NAT st i < m holds

(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) )

assume that

A1: m > 0 and

A2: len p <= m ; :: thesis: for x being Element of L

for i being Element of NAT st i < m holds

(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)

let x be Element of L; :: thesis: for i being Element of NAT st i < m holds

(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)

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)

(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) ; :: thesis: verum

for m being Element of NAT st m > 0 & len p <= m holds

for x being Element of L

for i being Element of NAT st i < m holds

(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)

let p be Polynomial of L; :: thesis: for m being Element of NAT st m > 0 & len p <= m holds

for x being Element of L

for i being Element of NAT st i < m holds

(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)

let m be Element of NAT ; :: thesis: ( m > 0 & len p <= m implies for x being Element of L

for i being Element of NAT st i < m holds

(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) )

assume that

A1: m > 0 and

A2: len p <= m ; :: thesis: for x being Element of L

for i being Element of NAT st i < m holds

(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)

let x be Element of L; :: thesis: for i being Element of NAT st i < m holds

(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)

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)

proof

hence
for i being Element of NAT st i < m holds
A3:
for k being Nat st k < m holds

(Col ((mConv (p,m)),1)) . (k + 1) = p . k

.= 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: ( i < m implies (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) )

assume A11: i < m ; :: thesis: (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)

A12: for k being Nat st k < m holds

(Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1))

(Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k))

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

(mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1)))

( 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: verum

end;(Col ((mConv (p,m)),1)) . (k + 1) = p . k

proof

A6: width (VM (x,m)) =
m
by MATRIX_0:24
let k be Nat; :: thesis: ( k < m implies (Col ((mConv (p,m)),1)) . (k + 1) = p . k )

assume A4: k < m ; :: thesis: (Col ((mConv (p,m)),1)) . (k + 1) = p . k

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: verum

end;assume A4: k < m ; :: thesis: (Col ((mConv (p,m)),1)) . (k + 1) = p . k

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: verum

.= 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: ( i < m implies (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) )

assume A11: i < m ; :: thesis: (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1)

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

A13:
for k being Nat st k < m holds
let k be Nat; :: thesis: ( k < m implies (Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1)) )

assume k < m ; :: thesis: (Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1))

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: verum

end;assume k < m ; :: thesis: (Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1))

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: verum

(Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k))

proof

A17:
for k being Nat
let k be Nat; :: thesis: ( k < m implies (Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k)) )

assume A14: k < m ; :: thesis: (Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k))

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: verum

end;assume A14: k < m ; :: thesis: (Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k))

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: verum

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

A21:
for k being Element of NAT st 1 <= k & k <= m holds
let k be Nat; :: thesis: 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

let a, b, c be Element of L; :: thesis: ( a = (Line ((VM (x,m)),(i + 1))) . (k + 1) & b = (Col ((mConv (p,m)),1)) . (k + 1) & c = p . k & k < m implies a * b = (pow (x,(i * k))) * c )

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 * b = (pow (x,(i * k))) * c

a = pow (x,(i * k)) by A13, A18, A20;

hence a * b = (pow (x,(i * k))) * c by A3, A19, A20; :: thesis: verum

end;a * b = (pow (x,(i * k))) * c

let a, b, c be Element of L; :: thesis: ( a = (Line ((VM (x,m)),(i + 1))) . (k + 1) & b = (Col ((mConv (p,m)),1)) . (k + 1) & c = p . k & k < m implies a * b = (pow (x,(i * k))) * c )

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 * b = (pow (x,(i * k))) * c

a = pow (x,(i * k)) by A13, A18, A20;

hence a * b = (pow (x,(i * k))) * c by A3, A19, A20; :: thesis: verum

(mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1)))

proof

A33:
Sum (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = eval (p,(x |^ i))
A22:
len (mConv (p,m)) = m
by A1, Th28;

let k be Element of NAT ; :: thesis: ( 1 <= k & k <= m implies (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) )

assume that

A23: 1 <= k and

A24: k <= m ; :: thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1)))

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

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: verum

end;let k be Element of NAT ; :: thesis: ( 1 <= k & k <= m implies (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) )

assume that

A23: 1 <= k and

A24: k <= m ; :: thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1)))

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

reconsider d = pow (x,(i * (k - 1))) as Element of L ;
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: verum

end;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: verum

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: verum

proof

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

.= 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 ) )

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

(mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k

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: verum

end;(mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L

proof

len (Line ((VM (x,m)),(i + 1))) =
width (VM (x,m))
by MATRIX_0:def 7
A35:
1 <= 1 + (len p)
by NAT_1:11;

let k be Nat; :: thesis: ( len p < k & k <= m implies (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L )

assume that

A36: len p < k and

A37: k <= m ; :: thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L

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: verum

end;let k be Nat; :: thesis: ( len p < k & k <= m implies (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L )

assume that

A36: len p < k and

A37: k <= m ; :: thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L

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: verum

.= 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

then consider G being FinSequence of L such that
defpred S_{1}[ 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_{1}[n,x]
;

ex G being FinSequence of L st

( dom G = Seg lengthG & ( for nn being Nat st nn in Seg lengthG holds

S_{1}[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: verum

end;A45: for n being Nat st n in Seg lengthG holds

ex x being Element of L st S

ex G being FinSequence of L st

( dom G = Seg lengthG & ( for nn being Nat st nn in Seg lengthG holds

S

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: verum

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

for k being Nat st k in dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) holds
let k be Element of NAT ; :: thesis: ( 1 <= k & k <= len p implies F . k = (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k )

assume that

A52: 1 <= k and

A53: k <= len p ; :: thesis: F . k = (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k

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: verum

end;assume that

A52: 1 <= k and

A53: k <= len p ; :: thesis: F . k = (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k

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: verum

(mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k

proof

then
mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1))) = F ^ G
by A50, FINSEQ_1:13;
let k be Nat; :: thesis: ( k in dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) implies (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k )

(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: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k

end;(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: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k

per cases
( ( 1 <= k & k <= len F ) or ( len F < k & k <= m ) )
by A50, A56, A55, FINSEQ_1:1;

end;

suppose A57:
( 1 <= k & k <= len F )
; :: thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k

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: verum

end;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: verum

suppose A58:
( len F < k & k <= m )
; :: thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k

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: verum

end;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: verum

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: verum

( 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: verum

(DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) ; :: thesis: verum