let GF be Field; :: thesis: for V being VectSp of GF
for L being Linear_Combination of V
for F being FinSequence of the carrier of V st Carrier L misses rng F holds
Sum (L (#) F) = 0. V
let V be VectSp of GF; :: thesis: for L being Linear_Combination of V
for F being FinSequence of the carrier of V st Carrier L misses rng F holds
Sum (L (#) F) = 0. V
let L be Linear_Combination of V; :: thesis: for F being FinSequence of the carrier of V st Carrier L misses rng F holds
Sum (L (#) F) = 0. V
defpred S1[ FinSequence] means for G being FinSequence of the carrier of V st G = $1 & Carrier L misses rng G holds
Sum (L (#) G) = 0. V;
A1: for p being FinSequence
for x being object st S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence; :: thesis: for x being object st S1[p] holds
S1[p ^ <*x*>]
let x be object ; :: thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A2: S1[p] ; :: thesis: S1[p ^ <*x*>]
let G be FinSequence of the carrier of V; :: thesis: ( G = p ^ <*x*> & Carrier L misses rng G implies Sum (L (#) G) = 0. V )
assume A3: G = p ^ <*x*> ; :: thesis: ( not Carrier L misses rng G or Sum (L (#) G) = 0. V )
then reconsider p = p, x9 = <*x*> as FinSequence of the carrier of V by FINSEQ_1:36;
x in {x} by TARSKI:def 1;
then A4: x in rng x9 by FINSEQ_1:38;
rng x9 c= the carrier of V by FINSEQ_1:def 4;
then reconsider x = x as Vector of V by A4;
assume Carrier L misses rng G ; :: thesis: Sum (L (#) G) = 0. V
then A5: {} = (Carrier L) /\ (rng G) by XBOOLE_0:def 7
.= (Carrier L) /\ ((rng p) \/ (rng <*x*>)) by A3, FINSEQ_1:31
.= (Carrier L) /\ ((rng p) \/ {x}) by FINSEQ_1:38
.= ((Carrier L) /\ (rng p)) \/ ((Carrier L) /\ {x}) by XBOOLE_1:23 ;
then (Carrier L) /\ (rng p) = {} ;
then Carrier L misses rng p by XBOOLE_0:def 7;
then A6: Sum (L (#) p) = 0. V by A2;
now :: thesis: not x in Carrier L
A7: x in {x} by TARSKI:def 1;
assume x in Carrier L ; :: thesis: contradiction
then x in (Carrier L) /\ {x} by A7, XBOOLE_0:def 4;
hence contradiction by A5; :: thesis: verum
end;
then A8: L . x = 0. GF by VECTSP_6:2;
Sum (L (#) G) = Sum ((L (#) p) ^ (L (#) x9)) by A3, VECTSP_6:13
.= (Sum (L (#) p)) + (Sum (L (#) x9)) by RLVECT_1:41
.= (0. V) + (Sum <*((L . x) * x)*>) by A6, VECTSP_6:10
.= Sum <*((L . x) * x)*> by RLVECT_1:4
.= (0. GF) * x by A8, RLVECT_1:44
.= 0. V by VECTSP_1:15 ;
hence Sum (L (#) G) = 0. V ; :: thesis: verum
end;
A9: S1[ {} ]
proof
let G be FinSequence of the carrier of V; :: thesis: ( G = {} & Carrier L misses rng G implies Sum (L (#) G) = 0. V )
assume G = {} ; :: thesis: ( not Carrier L misses rng G or Sum (L (#) G) = 0. V )
then A10: L (#) G = <*> the carrier of V by VECTSP_6:9;
assume Carrier L misses rng G ; :: thesis: Sum (L (#) G) = 0. V
thus Sum (L (#) G) = 0. V by A10, RLVECT_1:43; :: thesis: verum
end;
A11: for p being FinSequence holds S1[p] from FINSEQ_1:sch 3(A9, A1);
 let F be FinSequence of the carrier of V; :: thesis: ( Carrier L misses rng F implies Sum (L (#) F) = 0. V )
assume Carrier L misses rng F ; :: thesis: Sum (L (#) F) = 0. V
hence Sum (L (#) F) = 0. V by A11; :: thesis: verum