let V be RealLinearSpace; :: thesis: 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; :: thesis: 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; :: thesis: for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)
let P be Permutation of (dom F); :: thesis: ( G = F * P implies Sum (L (#) F) = Sum (L (#) G) )
assume A1: G = F * P ; :: thesis: Sum (L (#) F) = Sum (L (#) G)
set p = L (#) F;
set q = L (#) G;
len F = len (L (#) F) by RLVECT_2:def 9;
then A2: dom F = dom (L (#) F) by FINSEQ_3:31;
then reconsider r = (L (#) F) * P as FinSequence of the carrier of V by FINSEQ_2:51;
A3: ( len (L (#) F) = len F & len (L (#) G) = len G ) by RLVECT_2:def 9;
A4: len G = len F by A1, FINSEQ_2:48;
then A5: dom (L (#) F) = dom (L (#) G) by A3, FINSEQ_3:31;
A6: dom F = dom G by A4, FINSEQ_3:31;
A7: dom F = dom (L (#) F) by A3, FINSEQ_3:31;
len r = len (L (#) F) by A2, FINSEQ_2:48;
then A8: ( dom r = dom (L (#) F) & dom r = dom (L (#) F) ) by FINSEQ_3:31;

A9: now

let k be Nat; :: thesis: ( k in dom (L (#) G) implies (L (#) G) . k = r . k )
assume A10: k in dom (L (#) G) ; :: thesis: (L (#) G) . k = r . k
set l = P . k;
( dom P = dom F & rng P = dom F ) by FUNCT_2:67, FUNCT_2:def 3;
then A11: P . k in dom F by A5, A7, A10, FUNCT_1:def 5;
then reconsider l = P . k as Element of NAT ;
G /. k = G . k by A5, A6, A7, A10, PARTFUN1:def 8
.= F . (P . k) by A1, A5, A6, A7, A10, FUNCT_1:22
.= F /. l by A11, PARTFUN1:def 8 ;
then (L (#) G) . k = (L . (F /. l)) * (F /. l) by A10, RLVECT_2:def 9
.= (L (#) F) . (P . k) by A7, A11, RLVECT_2:def 9
.= r . k by A5, A8, A10, FUNCT_1:22 ;
hence (L (#) G) . k = r . k ; :: thesis: verum

end;

thus Sum (L (#) F) = Sum r by A2, RLVECT_2:9
.= Sum (L (#) G) by A5, A8, A9, FINSEQ_1:17 ; :: thesis: verum