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