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 :: 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 A5, A3, A7, FUNCT_1:11; :: 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 A8, A9, FUNCT_1:3;
(Func_Seq (I,p)) . s = (I * p) . i by BHSP_5:def 4
.= I . (p . i) by A8, A9, FUNCT_1:13
.= 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:2;
hence setsum Y = setopfunc (Y, the carrier of X, the carrier of X,I, the addF of X) by A1, A2, A3, A4, BHSP_5:def 5; :: thesis: verum