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)

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

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 )

then A8:
dom (Func_Seq (I,p)) = dom p
by TARSKI:2;( 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;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

now :: thesis: for s being object st s in dom (Func_Seq (I,p)) holds

(Func_Seq (I,p)) . s = p . s

then
Func_Seq (I,p) = p
by A8, FUNCT_1:2;(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;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

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