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)
set p = L (#) F;
set q = 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)
A2: len G = len F by A1, FINSEQ_2:44;
len F = len (L (#) F) by RLVECT_2:def 7;
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 RLVECT_2:def 7;
then A6: dom F = dom (L (#) F) by FINSEQ_3:29;
len (L (#) G) = len G by RLVECT_2:def 7;
then A7: dom (L (#) F) = dom (L (#) G) by A5, A2, FINSEQ_3:29;
A8: dom F = dom G by A2, FINSEQ_3:29;

A9: now :: thesis: for k being Nat st k in dom (L (#) G) holds
(L (#) G) . k = r . k

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:52, FUNCT_2:def 3;
then A11: P . k in dom F by A7, A6, A10, FUNCT_1:def 3;
then reconsider l = P . k as Element of NAT ;
G /. k = G . k by A7, A8, A6, A10, PARTFUN1:def 6
.= F . (P . k) by A1, A7, A8, A6, A10, FUNCT_1:12
.= F /. l by A11, PARTFUN1:def 6 ;
then (L (#) G) . k = (L . (F /. l)) * (F /. l) by A10, RLVECT_2:def 7
.= (L (#) F) . (P . k) by A6, A11, RLVECT_2:def 7
.= r . k by A7, A4, A10, FUNCT_1:12 ;
hence (L (#) G) . k = r . k ; :: thesis: verum

end;

thus Sum (L (#) F) = Sum r by A3, RLVECT_2:7
.= Sum (L (#) G) by A7, A4, A9, FINSEQ_1:13 ; :: thesis: verum