let V be RealLinearSpace; :: thesis: for F being FinSequence of the carrier of V st F is one-to-one holds

for L being Linear_Combination of V st Carrier L c= rng F holds

Sum (L (#) F) = Sum L

let F be FinSequence of the carrier of V; :: thesis: ( F is one-to-one implies for L being Linear_Combination of V st Carrier L c= rng F holds

Sum (L (#) F) = Sum L )

assume A1: F is one-to-one ; :: thesis: for L being Linear_Combination of V st Carrier L c= rng F holds

Sum (L (#) F) = Sum L

rng F c= rng F ;

then reconsider X = rng F as Subset of (rng F) ;

let L be Linear_Combination of V; :: thesis: ( Carrier L c= rng F implies Sum (L (#) F) = Sum L )

assume A2: Carrier L c= rng F ; :: thesis: Sum (L (#) F) = Sum L

consider G being FinSequence of the carrier of V such that

A3: G is one-to-one and

A4: rng G = Carrier L and

A5: Sum L = Sum (L (#) G) by RLVECT_2:def 8;

reconsider A = rng G as Subset of (rng F) by A2, A4;

set F1 = F - (A `);

X \ (A `) = X /\ ((A `) `) by SUBSET_1:13

.= A by XBOOLE_1:28 ;

then A6: rng (F - (A `)) = rng G by FINSEQ_3:65;

F - (A `) is one-to-one by A1, FINSEQ_3:87;

then F - (A `),G are_fiberwise_equipotent by A3, A6, RFINSEQ:26;

then A7: ex Q being Permutation of (dom G) st F - (A `) = G * Q by RFINSEQ:4;

reconsider F1 = F - (A `), F2 = F - A as FinSequence of the carrier of V by FINSEQ_3:86;

A8: (rng F) \ (rng G) misses rng G by XBOOLE_1:79;

(rng F2) /\ (rng G) = ((rng F) \ (rng G)) /\ (rng G) by FINSEQ_3:65

.= {} by A8, XBOOLE_0:def 7 ;

then A9: Carrier L misses rng F2 by A4, XBOOLE_0:def 7;

ex P being Permutation of (dom F) st (F - (A `)) ^ (F - A) = F * P by FINSEQ_3:115;

then Sum (L (#) F) = Sum (L (#) (F1 ^ F2)) by Th4

.= Sum ((L (#) F1) ^ (L (#) F2)) by RLVECT_3:34

.= (Sum (L (#) F1)) + (Sum (L (#) F2)) by RLVECT_1:41

.= (Sum (L (#) F1)) + (0. V) by A9, Th5

.= (Sum (L (#) G)) + (0. V) by A7, Th4

.= Sum L by A5, RLVECT_1:4 ;

hence Sum (L (#) F) = Sum L ; :: thesis: verum

for L being Linear_Combination of V st Carrier L c= rng F holds

Sum (L (#) F) = Sum L

let F be FinSequence of the carrier of V; :: thesis: ( F is one-to-one implies for L being Linear_Combination of V st Carrier L c= rng F holds

Sum (L (#) F) = Sum L )

assume A1: F is one-to-one ; :: thesis: for L being Linear_Combination of V st Carrier L c= rng F holds

Sum (L (#) F) = Sum L

rng F c= rng F ;

then reconsider X = rng F as Subset of (rng F) ;

let L be Linear_Combination of V; :: thesis: ( Carrier L c= rng F implies Sum (L (#) F) = Sum L )

assume A2: Carrier L c= rng F ; :: thesis: Sum (L (#) F) = Sum L

consider G being FinSequence of the carrier of V such that

A3: G is one-to-one and

A4: rng G = Carrier L and

A5: Sum L = Sum (L (#) G) by RLVECT_2:def 8;

reconsider A = rng G as Subset of (rng F) by A2, A4;

set F1 = F - (A `);

X \ (A `) = X /\ ((A `) `) by SUBSET_1:13

.= A by XBOOLE_1:28 ;

then A6: rng (F - (A `)) = rng G by FINSEQ_3:65;

F - (A `) is one-to-one by A1, FINSEQ_3:87;

then F - (A `),G are_fiberwise_equipotent by A3, A6, RFINSEQ:26;

then A7: ex Q being Permutation of (dom G) st F - (A `) = G * Q by RFINSEQ:4;

reconsider F1 = F - (A `), F2 = F - A as FinSequence of the carrier of V by FINSEQ_3:86;

A8: (rng F) \ (rng G) misses rng G by XBOOLE_1:79;

(rng F2) /\ (rng G) = ((rng F) \ (rng G)) /\ (rng G) by FINSEQ_3:65

.= {} by A8, XBOOLE_0:def 7 ;

then A9: Carrier L misses rng F2 by A4, XBOOLE_0:def 7;

ex P being Permutation of (dom F) st (F - (A `)) ^ (F - A) = F * P by FINSEQ_3:115;

then Sum (L (#) F) = Sum (L (#) (F1 ^ F2)) by Th4

.= Sum ((L (#) F1) ^ (L (#) F2)) by RLVECT_3:34

.= (Sum (L (#) F1)) + (Sum (L (#) F2)) by RLVECT_1:41

.= (Sum (L (#) F1)) + (0. V) by A9, Th5

.= (Sum (L (#) G)) + (0. V) by A7, Th4

.= Sum L by A5, RLVECT_1:4 ;

hence Sum (L (#) F) = Sum L ; :: thesis: verum