let L be Field; :: thesis: 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))
let m be Element of NAT ; :: thesis: ( m > 0 implies 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)) )
assume A1: m > 0 ; :: thesis: 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))
let x be Element of L; :: thesis: ( x is_primitive_root_of_degree m implies (VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m)) )
assume A2: x is_primitive_root_of_degree m ; :: thesis: (VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m))
for i, j being Nat st i >= 1 & i <= m & j >= 1 & j <= m holds
((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j))

proof

let i, j be Nat; :: thesis: ( i >= 1 & i <= m & j >= 1 & j <= m implies ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) )
A3: ( i in NAT & j in NAT ) by ORDINAL1:def 12;
ex G being FinSequence of L st
( dom G = Seg m & ( for k being Nat st k in Seg m holds
G . k = pow (x,((i - j) * (k - 1))) ) )

proof

defpred S₁[ Nat, set ] means $2 = pow (x,((i - j) * ($1 - 1)));
A4: for n being Nat st n in Seg m holds
ex x being Element of L st S₁[n,x] ;
ex G being FinSequence of L st
( dom G = Seg m & ( for nn being Nat st nn in Seg m holds
S₁[nn,G . nn] ) ) from FINSEQ_1:sch 5(A4);
hence ex G being FinSequence of L st
( dom G = Seg m & ( for k being Nat st k in Seg m holds
G . k = pow (x,((i - j) * (k - 1))) ) ) ; :: thesis: verum

end;

then consider s being FinSequence of L such that
A5: dom s = Seg m and
A6: for k being Nat st k in Seg m holds
s . k = pow (x,((i - j) * (k - 1))) ;
A7: len s = m by A5, FINSEQ_1:def 3;
A8: for k being Nat st 1 <= k & k <= m holds
s /. k = pow (x,((i - j) * (k - 1)))

proof

let k be Nat; :: thesis: ( 1 <= k & k <= m implies s /. k = pow (x,((i - j) * (k - 1))) )
assume A9: ( 1 <= k & k <= m ) ; :: thesis: s /. k = pow (x,((i - j) * (k - 1)))
then A10: k in dom s by A5;
k in Seg m by A9;
then pow (x,((i - j) * (k - 1))) = s . k by A6
.= s /. k by A10, PARTFUN1:def 6 ;
hence s /. k = pow (x,((i - j) * (k - 1))) ; :: thesis: verum

end;

A11: Indices (1. (L,m)) = [:(Seg m),(Seg m):] by MATRIX_0:24;
assume that
A12: ( 1 <= i & i <= m ) and
A13: ( 1 <= j & j <= m ) ; :: thesis: ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j))

per cases ( i = j or i <> j ) ;

suppose A14: i = j ; :: thesis: ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j))

A15: for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L

proof

let k be Element of NAT ; :: thesis: ( 1 <= k & k <= m implies s /. k = 1. L )
assume ( 1 <= k & k <= m ) ; :: thesis: s /. k = 1. L
then s /. k = pow (x,((i - j) * (k - 1))) by A8
.= 1. L by A14, Th13 ;
hence s /. k = 1. L ; :: thesis: verum

end;

i in Seg m by A12;
then A16: [i,i] in Indices (1. (L,m)) by A11, ZFMISC_1:87;
((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s by A2, A3, A12, A13, A7, A8, Th37
.= m * (1. L) by A7, A15, Th4
.= (emb (m,L)) * (1. L) ;
hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) by A14, A16, MATRIX_1:def 3; :: thesis: verum

end;

suppose A17: i <> j ; :: thesis: ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j))

( i in Seg m & j in Seg m ) by A12, A13;
then A18: [i,j] in Indices (1. (L,m)) by A11, ZFMISC_1:87;
((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L by A2, A3, A12, A13, A17, Th38
.= (emb (m,L)) * (0. L) ;
hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) by A17, A18, MATRIX_1:def 3; :: thesis: verum

end;

end;

end;

hence (VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m)) by A1, Th36; :: thesis: verum