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;
assume A4: ( 1 <= i & i <= m & 1 <= j & j <= m ) ; :: thesis: ((VM x,m) * (VM (x " ),m)) * i,j = (emb m,L) * ((1. L,m) * i,j)
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));
A5: 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(A5);
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
A6: ( dom s = Seg m & ( for k being Nat st k in Seg m holds
s . k = pow x,((i - j) * (k - 1)) ) ) ;
A7: len s = m by A6, 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 Seg m by FINSEQ_1:3;
A11: k in dom s by A6, A9, FINSEQ_1:3;
pow x,((i - j) * (k - 1)) = s . k by A6, A10
.= s /. k by A11, PARTFUN1:def 8 ;
hence s /. k = pow x,((i - j) * (k - 1)) ; :: thesis: verum

end;

A12: ( len (1. L,m) = m & width (1. L,m) = m & Indices (1. L,m) = [:(Seg m),(Seg m):] ) by MATRIX_1:25;

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

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

((VM x,m) * (VM (x " ),m)) * i,j = (emb m,L) * ((1. L,m) * i,j)

proof

A14: 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 A13, Th13 ;
hence s /. k = 1. L ; :: thesis: verum

end;

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

end;

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

end;

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

((VM x,m) * (VM (x " ),m)) * i,j = (emb m,L) * ((1. L,m) * i,j)

proof

A17: ((VM x,m) * (VM (x " ),m)) * i,j = 0. L by A2, A3, A4, A16, Th38
.= (emb m,L) * (0. L) by VECTSP_1:36 ;
( i in Seg m & j in Seg m ) by A4, FINSEQ_1:3;
then [i,j] in Indices (1. L,m) by A12, ZFMISC_1:106;
hence ((VM x,m) * (VM (x " ),m)) * i,j = (emb m,L) * ((1. L,m) * i,j) by A16, A17, MATRIX_1:def 12; :: thesis: verum

end;

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

end;

end;

end;

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