let X be RealUnitarySpace; :: thesis: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity implies for S being finite Subset of X st not S is empty holds
for L being linear-Functional of X holds L . (setsum S) = setopfunc S,the carrier of X,REAL ,L,addreal )
assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity ) ; :: thesis: for S being finite Subset of X st not S is empty holds
for L being linear-Functional of X holds L . (setsum S) = setopfunc S,the carrier of X,REAL ,L,addreal
let S be finite Subset of X; :: thesis: ( not S is empty implies for L being linear-Functional of X holds L . (setsum S) = setopfunc S,the carrier of X,REAL ,L,addreal )
assume A2: not S is empty ; :: thesis: for L being linear-Functional of X holds L . (setsum S) = setopfunc S,the carrier of X,REAL ,L,addreal
let L be linear-Functional of X; :: thesis: L . (setsum S) = setopfunc S,the carrier of X,REAL ,L,addreal
A3: dom L = the carrier of X by FUNCT_2:def 1;
consider p being FinSequence of the carrier of X such that
A4: ( p is one-to-one & rng p = S & setsum S = the addF of X "**" p ) by A1, Def1;
reconsider q1 = Func_Seq L,p as FinSequence of REAL ;
A5: dom (Func_Seq L,p) = dom p

proof

now

let xd be set ; :: thesis: ( xd in dom (Func_Seq L,p) iff xd in dom p )
A6: ( xd in dom (Func_Seq L,p) iff xd in dom (L * p) ) by BHSP_5:def 4;
( xd in dom p implies p . xd in rng p ) by FUNCT_1:12;
hence ( xd in dom (Func_Seq L,p) iff xd in dom p ) by A3, A6, FUNCT_1:21; :: thesis: verum

end;

hence dom (Func_Seq L,p) = dom p by TARSKI:2; :: thesis: verum

end;

A7: for i being Element of NAT st i in dom p holds
q1 . i = L . (p . i)

proof

let i be Element of NAT ; :: thesis: ( i in dom p implies q1 . i = L . (p . i) )
assume A8: i in dom p ; :: thesis: q1 . i = L . (p . i)
q1 . i = (L * p) . i by BHSP_5:def 4
.= L . (p . i) by A8, FUNCT_1:23 ;
hence q1 . i = L . (p . i) ; :: thesis: verum

end;

len p >= 1

proof

card S <> 0 by A2;
then 0 < card S ;
then 0 + 1 <= card S by INT_1:20;
hence len p >= 1 by A4, FINSEQ_4:77; :: thesis: verum

end;

then L . (the addF of X "**" p) = addreal "**" q1 by A5, A7, Th4;
hence L . (setsum S) = setopfunc S,the carrier of X,REAL ,L,addreal by A3, A4, BHSP_5:def 5; :: thesis: verum