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;

.= Sum (L (#) G) by A7, A4, A9, FINSEQ_1:13 ; :: thesis: verum

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

thus Sum (L (#) F) =
Sum r
by A3, RLVECT_2:7
(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;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

.= Sum (L (#) G) by A7, A4, A9, FINSEQ_1:13 ; :: thesis: verum