for L being Field
for x being Element of L
for s being FinSequence of L
for i, j, m being Element of NAT st x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & ( for k being Nat st 1 <= k & k <= m holds
s /. k = pow (x,((i - j) * (k - 1))) ) holds
((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s