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 A1: ( i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m ) ; :: thesis: ((VM x,m) * (VM (x " ),m)) * i,j = 0. L
then A2: x <> 0. L by Th30;
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));
A3: 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(A3);
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
A4: ( dom s = Seg m & ( for k being Nat st k in Seg m holds
s . k = pow x,((i - j) * (k - 1)) ) ) ;
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 A5: ( 1 <= k & k <= m ) ; :: thesis: s /. k = pow x,((i - j) * (k - 1))
then A6: k in Seg m by FINSEQ_1:3;
A7: k in dom s by A4, A5, FINSEQ_1:3;
pow x,((i - j) * (k - 1)) = s . k by A4, A6
.= s /. k by A7, PARTFUN1:def 8 ;
hence s /. k = pow x,((i - j) * (k - 1)) ; :: thesis: verum

end;

then A8: ( len s = m & ( for k being Nat st 1 <= k & k <= m holds
s /. k = pow x,((i - j) * (k - 1)) ) ) by A4, FINSEQ_1:def 3;
A9: pow x,(m * (i - j)) = pow (pow x,m),(i - j) by A2, Th26
.= pow (x |^ m),(i - j) by Def3
.= pow (1. L),(i - j) by A1, Def6
.= 1. L by Th16 ;
A10: pow x,(i - j) <> 1. L by A1, Th32;
A11: 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 A12: ( 1 <= k & k <= len s ) ; :: thesis: s . k = (pow x,(i - j)) |^ (k -' 1)
then A13: 1 - 1 <= k - 1 by XREAL_1:11;
s . k = s /. k by A12, FINSEQ_4:24
.= pow x,((i - j) * (k - 1)) by A8, A12
.= pow x,((i - j) * (k -' 1)) by A13, XREAL_0:def 2
.= pow (pow x,(i - j)),(k -' 1) by A2, Th26
.= (pow x,(i - j)) |^ (k -' 1) by Def3 ;
hence s . k = (pow x,(i - j)) |^ (k -' 1) ; :: thesis: verum

end;

consider r being Element of L such that
A14: r = pow x,(i - j) ;
Sum s = ((1. L) - ((pow x,(i - j)) |^ (len s))) / ((1. L) - (pow x,(i - j))) by A10, A11, Th5
.= ((1. L) - ((pow x,(i - j)) |^ m)) / ((1. L) - (pow x,(i - j))) by A4, FINSEQ_1:def 3
.= ((1. L) - (pow (pow x,(i - j)),m)) / ((1. L) - (pow x,(i - j))) by Def3
.= ((1. L) - (pow x,((i - j) * m))) / ((1. L) - (pow x,(i - j))) by A2, Th26
.= (0. L) / ((1. L) - r) by A9, A14, VECTSP_1:66
.= 0. L by VECTSP_1:39 ;
hence ((VM x,m) * (VM (x " ),m)) * i,j = 0. L by A1, A8, Th37; :: thesis: verum