let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for F being FinSequence of V1
for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds
Sum (KL (#) F) = Sum KL
let V1 be finite-dimensional VectSp of K; :: thesis: for F being FinSequence of V1
for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds
Sum (KL (#) F) = Sum KL
let F be FinSequence of V1; :: thesis: for KL being Linear_Combination of V1 st F is one-to-one & Carrier KL c= rng F holds
Sum (KL (#) F) = Sum KL
let KL be Linear_Combination of V1; :: thesis: ( F is one-to-one & Carrier KL c= rng F implies Sum (KL (#) F) = Sum KL )
assume A1: F is one-to-one ; :: thesis: ( not Carrier KL c= rng F or Sum (KL (#) F) = Sum KL )
assume A2: Carrier KL c= rng F ; :: thesis: Sum (KL (#) F) = Sum KL
then reconsider A = Carrier KL as Subset of (rng F) ;
reconsider G1 = F - (A ` ), G2 = F - A as FinSequence of V1 by FINSEQ_3:93;
A3: G1 is one-to-one by A1, FINSEQ_3:94;
A4: rng G1 = (rng F) \ (A ` ) by FINSEQ_3:72
.= (rng F) \ ((rng F) \ (Carrier KL)) by SUBSET_1:def 5
.= (rng F) /\ (Carrier KL) by XBOOLE_1:48
.= Carrier KL by A2, XBOOLE_1:28 ;
for k being Nat st k in dom (KL (#) G2) holds
(KL (#) G2) /. k = 0. V1

proof

let k be Nat; :: thesis: ( k in dom (KL (#) G2) implies (KL (#) G2) /. k = 0. V1 )
assume A5: k in dom (KL (#) G2) ; :: thesis: (KL (#) G2) /. k = 0. V1
len (KL (#) G2) = len G2 by VECTSP_6:def 8;
then A6: dom (KL (#) G2) = dom G2 by FINSEQ_3:31;
then G2 . k in rng G2 by A5, FUNCT_1:def 5;
then G2 . k in (rng F) \ (Carrier KL) by FINSEQ_3:72;
then not G2 . k in Carrier KL by XBOOLE_0:def 5;
then A7: not G2 /. k in Carrier KL by A5, A6, PARTFUN1:def 8;
reconsider k1 = k as Element of NAT by ORDINAL1:def 13;
thus (KL (#) G2) /. k = (KL (#) G2) . k by A5, PARTFUN1:def 8
.= (KL . (G2 /. k1)) * (G2 /. k1) by A5, VECTSP_6:def 8
.= (0. K) * (G2 /. k) by A7, VECTSP_6:20
.= 0. V1 by VECTSP_1:59 ; :: thesis: verum

end;

then A8: Sum (KL (#) G2) = 0. V1 by Th15;
consider p1 being Permutation of (dom F) such that
A9: (F - (A ` )) ^ (F - A) = F * p1 by A1, FINSEQ_3:124;
len (KL (#) F) = len F by VECTSP_6:def 8;
then dom (KL (#) F) = dom F by FINSEQ_3:31;
then reconsider p1 = p1 as Permutation of (dom (KL (#) F)) ;
KL (#) (G1 ^ G2) = (KL (#) F) * p1 by A9, Th23;
hence Sum (KL (#) F) = Sum (KL (#) (G1 ^ G2)) by RLVECT_2:9
.= Sum ((KL (#) G1) ^ (KL (#) G2)) by VECTSP_6:37
.= (Sum (KL (#) G1)) + (Sum (KL (#) G2)) by RLVECT_1:58
.= (Sum KL) + (0. V1) by A3, A4, A8, VECTSP_6:def 9
.= Sum KL by RLVECT_1:10 ;
:: thesis: verum