let V be Z_Module; :: thesis: for L being Linear_Combination of V
for F being FinSequence 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 V st Carrier L misses rng F holds
Sum (L (#) F) = 0. V
defpred S₁[ FinSequence] means for G being FinSequence 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 S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence; :: thesis: for x being object st S₁[p] holds
S₁[p ^ <*x*>]
let x be object ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A2: S₁[p] ; :: thesis: S₁[p ^ <*x*>]
let G be FinSequence 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 V by FINSEQ_1:36;
x in {x} by TARSKI:def 1;
then A4: x in rng x9 by FINSEQ_1:38;
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 A6: Sum (L (#) p) = 0. V by A2, XBOOLE_0:def 7;
A7: (Carrier L) /\ {x} = {} by A5;

now :: thesis: not x in Carrier L

A8: x in {x} by TARSKI:def 1;
assume x in Carrier L ; :: thesis: contradiction
hence contradiction by A7, A8, XBOOLE_0:def 4; :: thesis: verum

end;

then A9: L . x = 0 ;
Sum (L (#) G) = Sum ((L (#) p) ^ (L (#) x9)) by A3, ZMODUL02:51
.= (Sum (L (#) p)) + (Sum (L (#) x9)) by RLVECT_1:41
.= (0. V) + (Sum <*((L . x) * x)*>) by A6, ZMODUL02:15
.= Sum <*((L . x) * x)*> by RLVECT_1:4
.= (0. INT.Ring) * x by A9, RLVECT_1:44
.= 0. V by ZMODUL01:1 ;
hence Sum (L (#) G) = 0. V ; :: thesis: verum

end;

A10: S₁[ {} ]

proof

let G be FinSequence 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 ZMODUL02:14;
assume Carrier L misses rng G ; :: thesis: Sum (L (#) G) = 0. V
thus Sum (L (#) G) = 0. V by A11, RLVECT_1:43; :: thesis: verum

end;

A12: for p being FinSequence holds S₁[p] from FINSEQ_1:sch 3(A10, A1);
let F be FinSequence 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