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:115;

reconsider G1 = F - (A `), G2 = F - A as FinSequence of V1 by FINSEQ_3:86;

A4: G1 is one-to-one by A1, FINSEQ_3:87;

len (KL (#) F) = len F by VECTSP_6:def 5;

then dom (KL (#) F) = dom F by FINSEQ_3:29;

then reconsider p1 = p1 as Permutation of (dom (KL (#) F)) ;

A5: rng G1 = (rng F) \ (A `) by FINSEQ_3:65

.= (rng F) \ ((rng F) \ (Carrier KL)) by SUBSET_1:def 4

.= (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

KL (#) (G1 ^ G2) = (KL (#) F) * p1 by A3, Th19;

hence Sum (KL (#) F) = Sum (KL (#) (G1 ^ G2)) by RLVECT_2:7

.= Sum ((KL (#) G1) ^ (KL (#) G2)) by VECTSP_6:13

.= (Sum (KL (#) G1)) + (Sum (KL (#) G2)) by RLVECT_1:41

.= (Sum KL) + (0. V1) by A4, A5, A9, VECTSP_6:def 6

.= Sum KL by RLVECT_1:4 ;

:: thesis: verum

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:115;

reconsider G1 = F - (A `), G2 = F - A as FinSequence of V1 by FINSEQ_3:86;

A4: G1 is one-to-one by A1, FINSEQ_3:87;

len (KL (#) F) = len F by VECTSP_6:def 5;

then dom (KL (#) F) = dom F by FINSEQ_3:29;

then reconsider p1 = p1 as Permutation of (dom (KL (#) F)) ;

A5: rng G1 = (rng F) \ (A `) by FINSEQ_3:65

.= (rng F) \ ((rng F) \ (Carrier KL)) by SUBSET_1:def 4

.= (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

then A9:
Sum (KL (#) G2) = 0. V1
by Th11;
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 5;

then A7: dom (KL (#) G2) = dom G2 by FINSEQ_3:29;

then G2 . k in rng G2 by A6, FUNCT_1:def 3;

then G2 . k in (rng F) \ (Carrier KL) by FINSEQ_3:65;

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 6;

reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

thus (KL (#) G2) /. k = (KL (#) G2) . k by A6, PARTFUN1:def 6

.= (KL . (G2 /. k1)) * (G2 /. k1) by A6, VECTSP_6:def 5

.= (0. K) * (G2 /. k) by A8, VECTSP_6:2

.= 0. V1 by VECTSP_1:14 ; :: thesis: verum

end;assume A6: k in dom (KL (#) G2) ; :: thesis: (KL (#) G2) /. k = 0. V1

len (KL (#) G2) = len G2 by VECTSP_6:def 5;

then A7: dom (KL (#) G2) = dom G2 by FINSEQ_3:29;

then G2 . k in rng G2 by A6, FUNCT_1:def 3;

then G2 . k in (rng F) \ (Carrier KL) by FINSEQ_3:65;

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 6;

reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

thus (KL (#) G2) /. k = (KL (#) G2) . k by A6, PARTFUN1:def 6

.= (KL . (G2 /. k1)) * (G2 /. k1) by A6, VECTSP_6:def 5

.= (0. K) * (G2 /. k) by A8, VECTSP_6:2

.= 0. V1 by VECTSP_1:14 ; :: thesis: verum

KL (#) (G1 ^ G2) = (KL (#) F) * p1 by A3, Th19;

hence Sum (KL (#) F) = Sum (KL (#) (G1 ^ G2)) by RLVECT_2:7

.= Sum ((KL (#) G1) ^ (KL (#) G2)) by VECTSP_6:13

.= (Sum (KL (#) G1)) + (Sum (KL (#) G2)) by RLVECT_1:41

.= (Sum KL) + (0. V1) by A4, A5, A9, VECTSP_6:def 6

.= Sum KL by RLVECT_1:4 ;

:: thesis: verum