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
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 A2: ( Y c= dom I & ( 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
consider p being FinSequence of the carrier of X such that
A3: ( p is one-to-one & rng p = Y & setsum Y = the addF of X "**" p ) by A1, Def1;
A4: dom (Func_Seq I,p) = dom p

proof

now

let xd be set ; :: thesis: ( xd in dom (Func_Seq I,p) iff xd in dom p )
A5: ( xd in dom (Func_Seq I,p) iff xd in dom (I * 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 I,p) iff xd in dom p ) by A2, A3, A5, FUNCT_1:21; :: thesis: verum

end;

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

end;

now

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

end;

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