let S be non empty addLoopStr ; :: thesis: for LS being Linear_Combination of S
for F being FinSequence of S st Carrier LS misses rng F holds
Sum (LS * F) = 0
let LS be Linear_Combination of S; :: thesis: for F being FinSequence of S st Carrier LS misses rng F holds
Sum (LS * F) = 0
let F be FinSequence of S; :: thesis: ( Carrier LS misses rng F implies Sum (LS * F) = 0 )
assume A1: Carrier LS misses rng F ; :: thesis: Sum (LS * F) = 0
set LF = LS * F;
set LF0 = (len (LS * F)) |-> 0;

A2: now

let k be Nat; :: thesis: ( 1 <= k & k <= len (LS * F) implies (LS * F) . k = ((len (LS * F)) |-> 0) . k )
assume A3: ( 1 <= k & k <= len (LS * F) ) ; :: thesis: (LS * F) . k = ((len (LS * F)) |-> 0) . k
then k in Seg (len (LS * F)) by FINSEQ_1:1;
then A4: ((len (LS * F)) |-> 0) . k = 0 by FINSEQ_2:57;
A5: k in dom (LS * F) by A3, FINSEQ_3:25;
then k in dom F by FUNCT_1:11;
then F . k in rng F by FUNCT_1:def 3;
then A6: ( dom LS = the carrier of S & not F . k in Carrier LS ) by A1, FUNCT_2:def 1, XBOOLE_0:3;
( (LS * F) . k = LS . (F . k) & F . k in dom LS ) by A5, FUNCT_1:11, FUNCT_1:12;
hence (LS * F) . k = ((len (LS * F)) |-> 0) . k by A4, A6; :: thesis: verum

end;

len ((len (LS * F)) |-> 0) = len (LS * F) by CARD_1:def 7;
then LS * F = (len (LS * F)) |-> 0 by A2, FINSEQ_1:14;
hence Sum (LS * F) = 0 by RVSUM_1:81; :: thesis: verum