let L be Field; :: thesis: 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))

let m be Element of NAT ; :: thesis: 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))

let x be Element of L; :: thesis: ( m > 0 & x is_primitive_root_of_degree m implies (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m)) )

assume that

0 < m and

A1: x is_primitive_root_of_degree m ; :: thesis: (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m))

x <> 0. L by A1, Th30;

then (VM ((x "),m)) * (VM (x,m)) = (VM ((x "),m)) * (VM (((x ") "),m)) by VECTSP_1:24

.= (emb (m,L)) * (1. (L,m)) by A1, Th31, Th39 ;

hence (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m)) by A1, Th39; :: thesis: verum

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))

let m be Element of NAT ; :: thesis: 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))

let x be Element of L; :: thesis: ( m > 0 & x is_primitive_root_of_degree m implies (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m)) )

assume that

0 < m and

A1: x is_primitive_root_of_degree m ; :: thesis: (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m))

x <> 0. L by A1, Th30;

then (VM ((x "),m)) * (VM (x,m)) = (VM ((x "),m)) * (VM (((x ") "),m)) by VECTSP_1:24

.= (emb (m,L)) * (1. (L,m)) by A1, Th31, Th39 ;

hence (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m)) by A1, Th39; :: thesis: verum