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 :: thesis: for k being Nat st 1 <= k & k <= len (LS * F) holds
(LS * F) . k = ((len (LS * F)) |-> 0) . k
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
A4: 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 A5: ( 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 A4, FUNCT_1:11, FUNCT_1:12;
hence (LS * F) . k = ((len (LS * F)) |-> 0) . k by A5; :: 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;
hence Sum (LS * F) = 0 by RVSUM_1:81; :: thesis: verum