let V be RealLinearSpace; :: 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: {} = () /\ (rng G) by XBOOLE_0:def 7
.= () /\ ((rng p) \/ ()) by
.= () /\ ((rng p) \/ {x}) by FINSEQ_1:38
.= (() /\ (rng p)) \/ (() /\ {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;
A7: (Carrier L) /\ {x} = {} by A5;
now :: thesis: not x in Carrier Lend;
then A9: L . x = 0 by RLVECT_2:19;
Sum (L (#) G) = Sum ((L (#) p) ^ (L (#) x9)) by
.= (Sum (L (#) p)) + (Sum (L (#) x9)) by RLVECT_1:41
.= (0. V) + (Sum <*((L . x) * x)*>) by
.= Sum <*((L . x) * x)*> by RLVECT_1:4
.= 0 * x by
.= 0. V by RLVECT_1:10 ;
hence Sum (L (#) G) = 0. V ; :: thesis: verum
end;
A10: 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 A11: L (#) G = <*> the carrier of V by RLVECT_2:25;
assume Carrier L misses rng G ; :: thesis: Sum (L (#) G) = 0. V
thus Sum (L (#) G) = 0. V by ; :: thesis: verum
end;
A12: for p being FinSequence holds S1[p] from 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 A12; :: thesis: verum