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;

then LS * F = (len (LS * F)) |-> 0 by A2;

hence Sum (LS * F) = 0 by RVSUM_1:81; :: thesis: verum

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

len ((len (LS * F)) |-> 0) = len (LS * F)
by CARD_1:def 7;(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;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

then LS * F = (len (LS * F)) |-> 0 by A2;

hence Sum (LS * F) = 0 by RVSUM_1:81; :: thesis: verum