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 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)
then A2: 0 + 1 <= card S by INT_1:7;
let L be linear-Functional of X; :: thesis: L . (setsum S) = setopfunc (S, the carrier of X,REAL,L,addreal)
consider p being FinSequence of the carrier of X such that
A3: ( p is one-to-one & rng p = S ) and
A4: setsum S = the addF of X "**" p by A1, Def1;
reconsider q1 = Func_Seq (L,p) as FinSequence of REAL ;
A5: for i being Nat st i in dom p holds
q1 . i = L . (p . i)

proof

let i be Nat; :: thesis: ( i in dom p implies q1 . i = L . (p . i) )
assume A6: i in dom p ; :: thesis: q1 . i = L . (p . i)
q1 . i = (L * p) . i by BHSP_5:def 4
.= L . (p . i) by A6, FUNCT_1:13 ;
hence q1 . i = L . (p . i) ; :: thesis: verum

end;

A7: dom L = the carrier of X by FUNCT_2:def 1;

now :: thesis: for xd being object holds
( xd in dom (Func_Seq (L,p)) iff xd in dom p )

let xd be object ; :: thesis: ( xd in dom (Func_Seq (L,p)) iff xd in dom p )
A8: ( xd in dom p implies p . xd in rng p ) by FUNCT_1:3;
( xd in dom (Func_Seq (L,p)) iff xd in dom (L * p) ) by BHSP_5:def 4;
hence ( xd in dom (Func_Seq (L,p)) iff xd in dom p ) by A7, A8, FUNCT_1:11; :: thesis: verum

end;

then A9: dom (Func_Seq (L,p)) = dom p by TARSKI:2;
len p >= 1 by A3, A2, FINSEQ_4:62;
then L . ( the addF of X "**" p) = addreal "**" q1 by A9, A5, Th4;
hence L . (setsum S) = setopfunc (S, the carrier of X,REAL,L,addreal) by A3, A4, BHSP_5:def 5; :: thesis: verum