for L being Field
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