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) ;
consider p1 being Permutation of (dom F) such that
A3: (F - (A ` )) ^ (F - A) = F * p1 by FINSEQ_3:124;
reconsider G1 = F - (A ` ), G2 = F - A as FinSequence of V1 by FINSEQ_3:93;
A4: G1 is one-to-one by A1, FINSEQ_3:94;
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)) ;
A5: 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 A6: k in dom (KL (#) G2) ; :: thesis: (KL (#) G2) /. k = 0. V1
len (KL (#) G2) = len G2 by VECTSP_6:def 8;
then A7: dom (KL (#) G2) = dom G2 by FINSEQ_3:31;
then G2 . k in rng G2 by A6, 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 A8: not G2 /. k in Carrier KL by A6, A7, PARTFUN1:def 8;
reconsider k1 = k as Element of NAT by ORDINAL1:def 13;
thus (KL (#) G2) /. k = (KL (#) G2) . k by A6, PARTFUN1:def 8
.= (KL . (G2 /. k1)) * (G2 /. k1) by A6, VECTSP_6:def 8
.= (0. K) * (G2 /. k) by A8, VECTSP_6:20
.= 0. V1 by VECTSP_1:59 ; :: thesis: verum

end;

then A9: Sum (KL (#) G2) = 0. V1 by Th15;
KL (#) (G1 ^ G2) = (KL (#) F) * p1 by A3, 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 A4, A5, A9, VECTSP_6:def 9
.= Sum KL by RLVECT_1:10 ;
:: thesis: verum