theorem Th39: :: POLYNOM8:39

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