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)

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

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

A7:
dom L = the carrier of X
by FUNCT_2:def 1;
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;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

now :: thesis: for xd being object holds

( xd in dom (Func_Seq (L,p)) iff xd in dom p )

then A9:
dom (Func_Seq (L,p)) = dom p
by TARSKI:2;( 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;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

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