let L be Field; :: thesis:
let x be Element of L; :: thesis:
let s be FinSequence of L; :: thesis:
let i, j, m be Element of NAT ; :: thesis:
assume that
A1: x is_primitive_root_of_degree m and
A2: ( 1 <= i & i <= m ) and
A3: 1 <= j and
A4: j <= m and
A5: len s = m and
A6: for k being Nat st 1 <= k & k <= m holds
s /. k = pow x,((i - j) * (k - 1)) ; :: thesis:
len (Line (VM x,m),i) = width (VM x,m) by MATRIX_1:def 8
.= m by MATRIX_1:25
.= len (VM (x " ),m) by MATRIX_1:25
.= len (Col (VM (x " ),m),j) by MATRIX_1:def 9 ;
then A7: len (mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) = len (Line (VM x,m),i) by MATRIX_3:8
.= width (VM x,m) by MATRIX_1:def 8
.= m by MATRIX_1:25 ;
A8: x <> 0. L by A1, Th30;
A9: for k being Nat st 1 <= k & k <= m holds
((Line (VM x,m),i) /. k) * ((Col (VM (x " ),m),j) /. k) = pow x,((i - j) * (k - 1))

proof

len (Col (VM (x " ),m),j) = len (VM (x " ),m) by MATRIX_1:def 9
.= m by MATRIX_1:25 ;
then A10: Seg m = dom (Col (VM (x " ),m),j) by FINSEQ_1:def 3;
len (Line (VM x,m),i) = width (VM x,m) by MATRIX_1:def 8
.= m by MATRIX_1:25 ;
then A11: Seg m = dom (Line (VM x,m),i) by FINSEQ_1:def 3;
A12: 1 - 1 <= j - 1 by A3, XREAL_1:11;
let k be Nat; :: thesis:
assume that
A13: 1 <= k and
A14: k <= m ; :: thesis:
( len (VM (x " ),m) = m & k in Seg m ) by A13, A14, FINSEQ_1:3, MATRIX_1:25;
then A15: k in dom (VM (x " ),m) by FINSEQ_1:def 3;
k in Seg m by A13, A14, FINSEQ_1:3;
then A16: (Line (VM x,m),i) /. k = (Line (VM x,m),i) . k by A11, PARTFUN1:def 8;
1 - 1 <= k - 1 by A13, XREAL_1:11;
then A17: (j - 1) * (k - 1) in NAT by A12, INT_1:16;
width (VM x,m) = m by MATRIX_1:25;
then k in Seg (width (VM x,m)) by A13, A14, FINSEQ_1:3;
then A18: (Line (VM x,m),i) . k = (VM x,m) * i,k by MATRIX_1:def 8;
k in Seg m by A13, A14, FINSEQ_1:3;
then A19: (Col (VM (x " ),m),j) /. k = (Col (VM (x " ),m),j) . k by A10, PARTFUN1:def 8;
(VM (x " ),m) * k,j = pow (x " ),((j - 1) * (k - 1)) by A3, A4, A13, A14, Def8
.= pow x,(- ((j - 1) * (k - 1))) by A8, A17, Th22 ;
then (Col (VM (x " ),m),j) . k = pow x,(- ((j - 1) * (k - 1))) by A15, MATRIX_1:def 9;
then ((Line (VM x,m),i) /. k) * ((Col (VM (x " ),m),j) /. k) = (pow x,((i - 1) * (k - 1))) * (pow x,(- ((j - 1) * (k - 1)))) by A2, A13, A14, A16, A18, A19, Def8
.= pow x,((i - j) * (k - 1)) by A8, Th23 ;
hence ((Line (VM x,m),i) /. k) * ((Col (VM (x " ),m),j) /. k) = pow x,((i - j) * (k - 1)) ; :: thesis:

end;

A20: for k being Nat st 1 <= k & k <= m holds
(mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) /. k = s /. k

proof

len (Col (VM (x " ),m),j) = len (VM (x " ),m) by MATRIX_1:def 9
.= m by MATRIX_1:25 ;
then A21: Seg m = dom (Col (VM (x " ),m),j) by FINSEQ_1:def 3;
let k be Nat; :: thesis:
len (Line (VM x,m),i) = width (VM x,m) by MATRIX_1:def 8
.= m by MATRIX_1:25 ;
then A22: Seg m = dom (Line (VM x,m),i) by FINSEQ_1:def 3;
assume A23: ( 1 <= k & k <= m ) ; :: thesis:
then A24: ((Line (VM x,m),i) /. k) * ((Col (VM (x " ),m),j) /. k) = pow x,((i - j) * (k - 1)) by A9
.= s /. k by A6, A23 ;
k in Seg m by A23, FINSEQ_1:3;
then A25: (Col (VM (x " ),m),j) . k = (Col (VM (x " ),m),j) /. k by A21, PARTFUN1:def 8;
Seg m = dom (mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) by A7, FINSEQ_1:def 3;
then A26: k in dom (mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) by A23, FINSEQ_1:3;
k in Seg m by A23, FINSEQ_1:3;
then (Line (VM x,m),i) . k = (Line (VM x,m),i) /. k by A22, PARTFUN1:def 8;
then (mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) . k = ((Line (VM x,m),i) /. k) * ((Col (VM (x " ),m),j) /. k) by A26, A25, FVSUM_1:73;
hence (mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) /. k = s /. k by A26, A24, PARTFUN1:def 8; :: thesis:

end;

A27: for k being Nat st k in dom (mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) holds
(mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) . k = s . k

proof

let k be Nat; :: thesis:
assume A28: k in dom (mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) ; :: thesis:
A29: Seg m = dom (mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) by A7, FINSEQ_1:def 3;
then A30: ( 1 <= k & k <= m ) by A28, FINSEQ_1:3;
A31: k in dom s by A5, A28, A29, FINSEQ_1:def 3;
(mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) . k = (mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) /. k by A28, PARTFUN1:def 8
.= s /. k by A20, A30
.= s . k by A31, PARTFUN1:def 8 ;
hence (mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) . k = s . k ; :: thesis:

end;

dom (mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) = Seg m by A7, FINSEQ_1:def 3
.= dom s by A5, FINSEQ_1:def 3 ;
then A32: Sum (mlt (Line (VM x,m),i),(Col (VM (x " ),m),j)) = Sum s by A27, FINSEQ_1:17;
width (VM x,m) = m by MATRIX_1:25;
then A33: width (VM x,m) = len (VM (x " ),m) by MATRIX_1:25;
A34: ( width (VM x,m) = m & len (VM (x " ),m) = m ) by MATRIX_1:25;
len (VM x,m) = m by MATRIX_1:25;
then A35: len ((VM x,m) * (VM (x " ),m)) = m by A34, MATRIX_3:def 4;
width (VM (x " ),m) = m by MATRIX_1:25;
then width ((VM x,m) * (VM (x " ),m)) = m by A34, MATRIX_3:def 4;
then (VM x,m) * (VM (x " ),m) is Matrix of m,L by A2, A35, MATRIX_1:20;
then A36: Indices ((VM x,m) * (VM (x " ),m)) = [:(Seg m),(Seg m):] by MATRIX_1:25;
( i in Seg m & j in Seg m ) by A2, A3, A4;
then [i,j] in Indices ((VM x,m) * (VM (x " ),m)) by A36, ZFMISC_1:def 2;
then ((VM x,m) * (VM (x " ),m)) * i,j = (Line (VM x,m),i) "*" (Col (VM (x " ),m),j) by A33, MATRIX_3:def 4;
hence ((VM x,m) * (VM (x " ),m)) * i,j = Sum s by A32, FVSUM_1:def 10; :: thesis: