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 ;
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 :: thesis: for xd being object holds
( xd in dom (Func_Seq (I,p)) iff xd in dom p )
let xd be object ; :: 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:3;
( 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 ; :: thesis: verum
end;
then A8: dom (Func_Seq (I,p)) = dom p by TARSKI:2;
now :: thesis: for s being object st s in dom (Func_Seq (I,p)) holds
(Func_Seq (I,p)) . s = p . s
let s be object ; :: 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 Nat ;
A10: p . i in rng p by ;
(Func_Seq (I,p)) . s = (I * p) . i by BHSP_5:def 4
.= I . (p . i) by
.= 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 ;
hence setsum Y = setopfunc (Y, the carrier of X, the carrier of X,I, the addF of X) by ; :: thesis: verum