let X be RealUnitarySpace; ( 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 )
; 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; ( 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
; 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; 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)
A7:
dom L = the carrier of X
by FUNCT_2:def 1;
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; verum