theorem Th40: :: POLYNOM8:40

for L being Field
for m being Element of NAT
for x being Element of L st m > 0 & x is_primitive_root_of_degree m holds
(VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m))