let S be non empty addLoopStr ; :: thesis: for LS being Linear_Combination of S

for v being Element of S st Carrier LS c= {v} holds

sum LS = LS . v

let LS be Linear_Combination of S; :: thesis: for v being Element of S st Carrier LS c= {v} holds

sum LS = LS . v

let v be Element of S; :: thesis: ( Carrier LS c= {v} implies sum LS = LS . v )

consider p being FinSequence such that

A1: rng p = {v} and

A2: p is one-to-one by FINSEQ_4:58;

reconsider p = p as FinSequence of S by A1, FINSEQ_1:def 4;

( dom LS = the carrier of S & p = <*v*> ) by A1, A2, FINSEQ_3:97, FUNCT_2:def 1;

then A3: LS * p = <*(LS . v)*> by FINSEQ_2:34;

assume Carrier LS c= {v} ; :: thesis: sum LS = LS . v

hence sum LS = Sum (LS * p) by A1, A2, Th30

.= LS . v by A3, RVSUM_1:73 ;

:: thesis: verum

for v being Element of S st Carrier LS c= {v} holds

sum LS = LS . v

let LS be Linear_Combination of S; :: thesis: for v being Element of S st Carrier LS c= {v} holds

sum LS = LS . v

let v be Element of S; :: thesis: ( Carrier LS c= {v} implies sum LS = LS . v )

consider p being FinSequence such that

A1: rng p = {v} and

A2: p is one-to-one by FINSEQ_4:58;

reconsider p = p as FinSequence of S by A1, FINSEQ_1:def 4;

( dom LS = the carrier of S & p = <*v*> ) by A1, A2, FINSEQ_3:97, FUNCT_2:def 1;

then A3: LS * p = <*(LS . v)*> by FINSEQ_2:34;

assume Carrier LS c= {v} ; :: thesis: sum LS = LS . v

hence sum LS = Sum (LS * p) by A1, A2, Th30

.= LS . v by A3, RVSUM_1:73 ;

:: thesis: verum