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 Y being finite Subset of X
for I being Function of the carrier of X,the carrier of X st Y c= dom I & ( for x being set st x in dom I holds
I . x = x ) holds
setsum Y = setopfunc Y,the carrier of X,the carrier of X,I,the addF of X )
assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity ) ; :: thesis: for Y being finite Subset of X
for I being Function of the carrier of X,the carrier of X st Y c= dom I & ( for x being set st x in dom I holds
I . x = x ) holds
setsum Y = setopfunc Y,the carrier of X,the carrier of X,I,the addF of X
let Y be finite Subset of X; :: thesis: for I being Function of the carrier of X,the carrier of X st Y c= dom I & ( for x being set st x in dom I holds
I . x = x ) holds
setsum Y = setopfunc Y,the carrier of X,the carrier of X,I,the addF of X
consider p being FinSequence of the carrier of X such that
A2: p is one-to-one and
A3: rng p = Y and
A4: setsum Y = the addF of X "**" p by A1, Def1;
let I be Function of the carrier of X,the carrier of X; :: thesis: ( Y c= dom I & ( for x being set st x in dom I holds
I . x = x ) implies setsum Y = setopfunc Y,the carrier of X,the carrier of X,I,the addF of X )
assume that
A5: Y c= dom I and
A6: for x being set st x in dom I holds
I . x = x ; :: thesis: setsum Y = setopfunc Y,the carrier of X,the carrier of X,I,the addF of X

now

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

end;

then A8: dom (Func_Seq I,p) = dom p by TARSKI:2;

now

let s be set ; :: thesis: ( s in dom (Func_Seq I,p) implies (Func_Seq I,p) . s = p . s )
assume A9: s in dom (Func_Seq I,p) ; :: thesis: (Func_Seq I,p) . s = p . s
then reconsider i = s as Element of NAT ;
A10: p . i in rng p by A8, A9, FUNCT_1:12;
(Func_Seq I,p) . s = (I * p) . i by BHSP_5:def 4
.= I . (p . i) by A8, A9, FUNCT_1:23
.= p . i by A5, A6, A3, A10 ;
hence (Func_Seq I,p) . s = p . s ; :: thesis: verum

end;

then Func_Seq I,p = p by A8, FUNCT_1:9;
hence setsum Y = setopfunc Y,the carrier of X,the carrier of X,I,the addF of X by A1, A5, A2, A3, A4, BHSP_5:def 5; :: thesis: verum