let V be RealLinearSpace; :: thesis:
let F be FinSequence of the carrier of V; :: thesis:
assume A1: F is one-to-one ; :: thesis:
let L be Linear_Combination of V; :: thesis:
assume A2: Carrier L c= rng F ; :: thesis:
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 10;
reconsider A = rng G as Subset of (rng F) by A2, A4;
consider P being Permutation of (dom F) such that
A6: (F - (A ` )) ^ (F - A) = F * P by A1, FINSEQ_3:124;
set F1 = F - (A ` );
rng F c= rng F ;
then reconsider X = rng F as Subset of (rng F) ;
X \ (A ` ) = X /\ ((A ` ) ` ) by SUBSET_1:32
.= A by XBOOLE_1:28 ;
then ( rng (F - (A ` )) = rng G & F - (A ` ) is one-to-one ) by A1, FINSEQ_3:72, FINSEQ_3:94;
then F - (A ` ),G are_fiberwise_equipotent by A3, RFINSEQ:39;
then consider Q being Permutation of (dom G) such that
A7: F - (A ` ) = G * Q by RFINSEQ:17;
reconsider F1 = F - (A ` ), F2 = F - A as FinSequence of the carrier of V by FINSEQ_3:93;
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:72
.= {} by A8, XBOOLE_0:def 7 ;
then A9: Carrier L misses rng F2 by A4, XBOOLE_0:def 7;
Sum (L (#) F) = Sum (L (#) (F1 ^ F2)) by A6, Th5
.= Sum ((L (#) F1) ^ (L (#) F2)) by RLVECT_3:41
.= (Sum (L (#) F1)) + (Sum (L (#) F2)) by RLVECT_1:58
.= (Sum (L (#) F1)) + (0. V) by A9, Th6
.= (Sum (L (#) G)) + (0. V) by A7, Th5
.= Sum L by A5, RLVECT_1:10 ;
hence Sum (L (#) F) = Sum L ; :: thesis: