let L be Field; :: thesis: for m, i, j being Element of NAT
for x being Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds
((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L
let m, i, j be Element of NAT ; :: thesis: for x being Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds
((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L
let x be Element of L; :: thesis: ( i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m implies ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L )
assume that
A1: i <> j and
A2: ( 1 <= i & i <= m & 1 <= j & j <= m ) and
A3: x is_primitive_root_of_degree m ; :: thesis: ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L
A4: x <> 0. L by A3, Th30;
then A5: pow (x,(m * (i - j))) = pow ((pow (x,m)),(i - j)) by Th26
.= pow ((x |^ m),(i - j)) by Def2
.= pow ((1. L),(i - j)) by A3
.= 1. L by Th16 ;
ex G being FinSequence of L st
( dom G = Seg m & ( for k being Nat st k in Seg m holds
G . k = pow (x,((i - j) * (k - 1))) ) )

proof

defpred S₁[ Nat, set ] means $2 = pow (x,((i - j) * ($1 - 1)));
A6: for n being Nat st n in Seg m holds
ex x being Element of L st S₁[n,x] ;
ex G being FinSequence of L st
( dom G = Seg m & ( for nn being Nat st nn in Seg m holds
S₁[nn,G . nn] ) ) from FINSEQ_1:sch 5(A6);
hence ex G being FinSequence of L st
( dom G = Seg m & ( for k being Nat st k in Seg m holds
G . k = pow (x,((i - j) * (k - 1))) ) ) ; :: thesis: verum

end;

then consider s being FinSequence of L such that
A7: dom s = Seg m and
A8: for k being Nat st k in Seg m holds
s . k = pow (x,((i - j) * (k - 1))) ;
A9: for k being Nat st 1 <= k & k <= m holds
s /. k = pow (x,((i - j) * (k - 1)))

proof

let k be Nat; :: thesis: ( 1 <= k & k <= m implies s /. k = pow (x,((i - j) * (k - 1))) )
assume A10: ( 1 <= k & k <= m ) ; :: thesis: s /. k = pow (x,((i - j) * (k - 1)))
then A11: k in dom s by A7;
k in Seg m by A10;
then pow (x,((i - j) * (k - 1))) = s . k by A8
.= s /. k by A11, PARTFUN1:def 6 ;
hence s /. k = pow (x,((i - j) * (k - 1))) ; :: thesis: verum

end;

consider r being Element of L such that
A12: r = pow (x,(i - j)) ;
A13: len s = m by A7, FINSEQ_1:def 3;
for k being Nat st 1 <= k & k <= len s holds
s . k = (pow (x,(i - j))) |^ (k -' 1)

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len s implies s . k = (pow (x,(i - j))) |^ (k -' 1) )
assume that
A14: 1 <= k and
A15: k <= len s ; :: thesis: s . k = (pow (x,(i - j))) |^ (k -' 1)
A16: 1 - 1 <= k - 1 by A14, XREAL_1:9;
s . k = s /. k by A14, A15, FINSEQ_4:15
.= pow (x,((i - j) * (k - 1))) by A9, A13, A14, A15
.= pow (x,((i - j) * (k -' 1))) by A16, XREAL_0:def 2
.= pow ((pow (x,(i - j))),(k -' 1)) by A4, Th26
.= (pow (x,(i - j))) |^ (k -' 1) by Def2 ;
hence s . k = (pow (x,(i - j))) |^ (k -' 1) ; :: thesis: verum

end;

then Sum s = ((1. L) - ((pow (x,(i - j))) |^ (len s))) / ((1. L) - (pow (x,(i - j)))) by A1, A2, A3, Th5, Th32
.= ((1. L) - ((pow (x,(i - j))) |^ m)) / ((1. L) - (pow (x,(i - j)))) by A7, FINSEQ_1:def 3
.= ((1. L) - (pow ((pow (x,(i - j))),m))) / ((1. L) - (pow (x,(i - j)))) by Def2
.= ((1. L) - (pow (x,((i - j) * m)))) / ((1. L) - (pow (x,(i - j)))) by A4, Th26
.= (0. L) / ((1. L) - r) by A5, A12, VECTSP_1:19
.= 0. L ;
hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L by A2, A3, A9, A13, Th37; :: thesis: verum