let GF be Field; for V being VectSp of GF
for L being Linear_Combination of V
for F, G being FinSequence of the carrier of V
for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)
let V be VectSp of GF; for L being Linear_Combination of V
for F, G being FinSequence of the carrier of V
for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)
let L be Linear_Combination of V; for F, G being FinSequence of the carrier of V
for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)
let F, G be FinSequence of the carrier of V; for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)
set p = L (#) F;
set q = L (#) G;
let P be Permutation of (dom F); ( G = F * P implies Sum (L (#) F) = Sum (L (#) G) )
assume A1:
G = F * P
; Sum (L (#) F) = Sum (L (#) G)
A2:
len G = len F
by A1, FINSEQ_2:44;
len F = len (L (#) F)
by VECTSP_6:def 5;
then A3:
dom F = dom (L (#) F)
by FINSEQ_3:29;
then reconsider r = (L (#) F) * P as FinSequence of the carrier of V by FINSEQ_2:47;
len r = len (L (#) F)
by A3, FINSEQ_2:44;
then A4:
dom r = dom (L (#) F)
by FINSEQ_3:29;
A5:
len (L (#) F) = len F
by VECTSP_6:def 5;
then A6:
dom F = dom (L (#) F)
by FINSEQ_3:29;
len (L (#) G) = len G
by VECTSP_6:def 5;
then A7:
dom (L (#) F) = dom (L (#) G)
by A5, A2, FINSEQ_3:29;
A8:
dom F = dom G
by A2, FINSEQ_3:29;
now for k being Nat st k in dom (L (#) G) holds
(L (#) G) . k = r . klet k be
Nat;
( k in dom (L (#) G) implies (L (#) G) . k = r . k )assume A9:
k in dom (L (#) G)
;
(L (#) G) . k = r . kset l =
P . k;
(
dom P = dom F &
rng P = dom F )
by FUNCT_2:52, FUNCT_2:def 3;
then A10:
P . k in dom F
by A7, A6, A9, FUNCT_1:def 3;
then reconsider l =
P . k as
Element of
NAT ;
G /. k =
G . k
by A7, A8, A6, A9, PARTFUN1:def 6
.=
F . (P . k)
by A1, A7, A8, A6, A9, FUNCT_1:12
.=
F /. l
by A10, PARTFUN1:def 6
;
then (L (#) G) . k =
(L . (F /. l)) * (F /. l)
by A9, VECTSP_6:def 5
.=
(L (#) F) . (P . k)
by A6, A10, VECTSP_6:def 5
.=
r . k
by A7, A4, A9, FUNCT_1:12
;
hence
(L (#) G) . k = r . k
;
verum end;
hence
Sum (L (#) F) = Sum (L (#) G)
by A3, A7, A4, FINSEQ_1:13, RLVECT_2:7; verum