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 13;
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, FINSEQ_1:3;
k in Seg m by A9, FINSEQ_1:3;
then pow x,((i - j) * (k - 1)) = s . k by A6
.= s /. k by A10, PARTFUN1:def 8 ;
hence s /. k = pow x,((i - j) * (k - 1)) ; :: thesis: verum

end;

A11: Indices (1. L,m) = [:(Seg m),(Seg m):] by MATRIX_1:25;
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, FINSEQ_1:3;
then A16: [i,i] in Indices (1. L,m) by A11, ZFMISC_1:106;
((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) by VECTSP_1:def 19 ;
hence ((VM x,m) * (VM (x " ),m)) * i,j = (emb m,L) * ((1. L,m) * i,j) by A14, A16, MATRIX_1:def 12; :: 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, FINSEQ_1:3;
then A18: [i,j] in Indices (1. L,m) by A11, ZFMISC_1:106;
((VM x,m) * (VM (x " ),m)) * i,j = 0. L by A2, A3, A12, A13, A17, Th38
.= (emb m,L) * (0. L) by VECTSP_1:36 ;
hence ((VM x,m) * (VM (x " ),m)) * i,j = (emb m,L) * ((1. L,m) * i,j) by A17, A18, MATRIX_1:def 12; :: thesis: verum

end;

end;

end;

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