:: BHSP_6 semantic presentation

begin


definition
let X be RealUnitarySpace;
assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity ) ;
let Y be finite Subset of X;
func setsum Y ->  Element of X means :Def1: :: BHSP_6:def 1
 ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & it = the addF of X "**" p );
existence
 ex b1 being Element of X ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b1 = the addF of X "**" p )
proof
consider p being FinSequence such that
A1: rng p = Y and
A2: p is one-to-one by FINSEQ_4:58;
reconsider q = p as FinSequence of the carrier of X by A1, FINSEQ_1:def_4;
 ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & the addF of X "**" q = the addF of X "**" p ) by A1, A2;
hence  ex b1 being Element of X ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b1 = the addF of X "**" p ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of X st ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b1 = the addF of X "**" p ) & ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b2 = the addF of X "**" p ) holds
b1 = b2
proof
let X1, X2 be Element of X; ::_thesis: ( ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & X1 = the addF of X "**" p ) & ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & X2 = the addF of X "**" p ) implies X1 = X2 )
assume that
A3: ex p1 being FinSequence of the carrier of X st
( p1 is one-to-one & rng p1 = Y & X1 = the addF of X "**" p1 ) and
A4: ex p2 being FinSequence of the carrier of X st
( p2 is one-to-one & rng p2 = Y & X2 = the addF of X "**" p2 ) ; ::_thesis: X1 = X2
consider p2 being FinSequence of the carrier of X such that
A5: ( p2 is one-to-one & rng p2 = Y ) and
A6: X2 = the addF of X "**" p2 by A4;
consider p1 being FinSequence of the carrier of X such that
A7: ( p1 is one-to-one & rng p1 = Y ) and
A8: X1 = the addF of X "**" p1 by A3;
 ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) by A7, A5, BHSP_5:1;
hence  X1 = X2 by A1, A8, A6, FINSOP_1:7; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines setsum BHSP_6:def_1_:_
 for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for Y being finite Subset of X
for b3 being Element of X holds
( b3 = setsum Y iff ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b3 = the addF of X "**" p ) );

theorem Th1: :: BHSP_6:1
for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
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)
proof
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_set_holds_
(_xd_in_dom_(Func_Seq_(I,p))_iff_xd_in_dom_p_)
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: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:1;
now__::_thesis:_for_s_being_set_st_s_in_dom_(Func_Seq_(I,p))_holds_
(Func_Seq_(I,p))_._s_=_p_._s
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: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, A5, A2, A3, A4, BHSP_5:def_5; ::_thesis: verum
end;

theorem Th2: :: BHSP_6:2
for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for Y1, Y2 being finite Subset of X st Y1 misses Y2 holds
for Z being finite Subset of X st Z = Y1 \/ Y2 holds
setsum Z = (setsum Y1) + (setsum Y2)
proof
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 Y1, Y2 being finite Subset of X st Y1 misses Y2 holds
for Z being finite Subset of X st Z = Y1 \/ Y2 holds
setsum Z = (setsum Y1) + (setsum Y2) )
assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity ) ; ::_thesis: for Y1, Y2 being finite Subset of X st Y1 misses Y2 holds
for Z being finite Subset of X st Z = Y1 \/ Y2 holds
setsum Z = (setsum Y1) + (setsum Y2)
reconsider I = id the carrier of X as Function of the carrier of X, the carrier of X ;
let Y1, Y2 be finite Subset of X; ::_thesis: ( Y1 misses Y2 implies for Z being finite Subset of X st Z = Y1 \/ Y2 holds
setsum Z = (setsum Y1) + (setsum Y2) )
assume A2: Y1 misses Y2 ; ::_thesis: for Z being finite Subset of X st Z = Y1 \/ Y2 holds
setsum Z = (setsum Y1) + (setsum Y2)
A3: dom I = the carrier of X by FUNCT_2:def_1;
let Z be finite Subset of X; ::_thesis: ( Z = Y1 \/ Y2 implies setsum Z = (setsum Y1) + (setsum Y2) )
assume  Z = Y1 \/ Y2 ; ::_thesis: setsum Z = (setsum Y1) + (setsum Y2)
then A4: setopfunc (Z, the carrier of X, the carrier of X,I, the addF of X) = (setopfunc (Y1, the carrier of X, the carrier of X,I, the addF of X)) + (setopfunc (Y2, the carrier of X, the carrier of X,I, the addF of X)) by A1, A2, A3, BHSP_5:14;
A5: for x being set st x in the carrier of X holds
I . x = x by FUNCT_1:18;
then  ( setsum Y1 = setopfunc (Y1, the carrier of X, the carrier of X,I, the addF of X) & setsum Y2 = setopfunc (Y2, the carrier of X, the carrier of X,I, the addF of X) ) by A1, A3, Th1;
hence  setsum Z = (setsum Y1) + (setsum Y2) by A1, A5, A3, A4, Th1; ::_thesis: verum
end;

begin

definition
let X be RealUnitarySpace;
let Y be Subset of X;
attrY is summable_set  means :Def2: :: BHSP_6:def 2
 ex x being Point of X st
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e ) );
end;

:: deftheorem Def2 defines summable_set BHSP_6:def_2_:_
 for X being RealUnitarySpace
for Y being Subset of X holds
( Y is summable_set iff ex x being Point of X st
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e ) ) );

definition
let X be RealUnitarySpace;
let Y be Subset of X;
assume A1: Y is summable_set ;
func sum Y ->  Point of X means :: BHSP_6:def 3
 for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(it - (setsum Y1)).|| < e ) );
existence
 ex b1 being Point of X st
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(b1 - (setsum Y1)).|| < e ) ) by A1, Def2;
uniqueness
 for b1, b2 being Point of X st ( for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(b1 - (setsum Y1)).|| < e ) ) ) & ( for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(b2 - (setsum Y1)).|| < e ) ) ) holds
b1 = b2
proof
let y1, y2 be Point of X; ::_thesis: ( ( for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(y1 - (setsum Y1)).|| < e ) ) ) & ( for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(y2 - (setsum Y1)).|| < e ) ) ) implies y1 = y2 )
assume that
A2: for e1 being Real st e1 > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(y1 - (setsum Y1)).|| < e1 ) ) and
A3: for e2 being Real st e2 > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(y2 - (setsum Y1)).|| < e2 ) ) ; ::_thesis: y1 = y2
A4: now__::_thesis:_for_e3_being_Real_st_e3_>_0_holds_
||.(y1_-_y2).||_<_e3
let e3 be Real; ::_thesis: ( e3 > 0 implies ||.(y1 - y2).|| < e3 )
assume A5: e3 > 0 ; ::_thesis: ||.(y1 - y2).|| < e3
set e4 = e3 / 2;
consider Y01 being finite Subset of X such that
 not Y01 is empty and
A6: Y01 c= Y and
A7: for Y1 being finite Subset of X st Y01 c= Y1 & Y1 c= Y holds
||.(y1 - (setsum Y1)).|| < e3 / 2 by A2, A5, XREAL_1:139;
consider Y02 being finite Subset of X such that
 not Y02 is empty and
A8: Y02 c= Y and
A9: for Y1 being finite Subset of X st Y02 c= Y1 & Y1 c= Y holds
||.(y2 - (setsum Y1)).|| < e3 / 2 by A3, A5, XREAL_1:139;
set Y00 = Y01 \/ Y02;
A10: ( (e3 / 2) + (e3 / 2) = e3 & Y01 c= Y01 \/ Y02 ) by XBOOLE_1:7;
A11: Y01 \/ Y02 c= Y by A6, A8, XBOOLE_1:8;
then  ||.(y2 - (setsum (Y01 \/ Y02))).|| < e3 / 2 by A9, XBOOLE_1:7;
then  ||.(- (y2 - (setsum (Y01 \/ Y02)))).|| < e3 / 2 by BHSP_1:31;
then  ||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).|| < e3 by A7, A11, A10, XREAL_1:8;
then  ||.((y1 - (setsum (Y01 \/ Y02))) + (- (y2 - (setsum (Y01 \/ Y02))))).|| + (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||) < (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||) + e3 by BHSP_1:30, XREAL_1:8;
then A12: (||.((y1 - (setsum (Y01 \/ Y02))) + (- (y2 - (setsum (Y01 \/ Y02))))).|| + (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||)) + (- (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||)) < (e3 + (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||)) + (- (||.(y1 - (setsum (Y01 \/ Y02))).|| + ||.(- (y2 - (setsum (Y01 \/ Y02)))).||)) by XREAL_1:8;
||.(y1 - y2).|| = ||.((y1 - y2) + (0. X)).|| by RLVECT_1:def_4
.= ||.((y1 - y2) + ((setsum (Y01 \/ Y02)) - (setsum (Y01 \/ Y02)))).|| by RLVECT_1:5
.= ||.(((y1 - y2) + (setsum (Y01 \/ Y02))) - (setsum (Y01 \/ Y02))).|| by RLVECT_1:def_3
.= ||.((y1 - (y2 - (setsum (Y01 \/ Y02)))) - (setsum (Y01 \/ Y02))).|| by RLVECT_1:29
.= ||.(y1 - ((setsum (Y01 \/ Y02)) + (y2 - (setsum (Y01 \/ Y02))))).|| by RLVECT_1:27
.= ||.((y1 - (setsum (Y01 \/ Y02))) - (y2 - (setsum (Y01 \/ Y02)))).|| by RLVECT_1:27
.= ||.((y1 - (setsum (Y01 \/ Y02))) + (- (y2 - (setsum (Y01 \/ Y02))))).|| ;
hence  ||.(y1 - y2).|| < e3 by A12; ::_thesis: verum
end;
 y1 = y2
proof
assume  y1 <> y2 ; ::_thesis: contradiction
then  y1 - y2 <> 0. X by VECTSP_1:19;
then A13: ||.(y1 - y2).|| <> 0 by BHSP_1:26;
 0 <= ||.(y1 - y2).|| by BHSP_1:28;
hence  contradiction by A4, A13; ::_thesis: verum
end;
hence  y1 = y2 ; ::_thesis: verum
end;
end;

:: deftheorem  defines sum BHSP_6:def_3_:_
 for X being RealUnitarySpace
for Y being Subset of X st Y is summable_set holds
for b3 being Point of X holds
( b3 = sum Y iff for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(b3 - (setsum Y1)).|| < e ) ) );

definition
let X be RealUnitarySpace;
let L be linear-Functional of X;
attrL is Lipschitzian  means :Def4: :: BHSP_6:def 4
 ex K being Real st
( K > 0 & ( for x being Point of X holds abs (L . x) <= K * ||.x.|| ) );
end;

:: deftheorem Def4 defines Lipschitzian BHSP_6:def_4_:_
 for X being RealUnitarySpace
for L being linear-Functional of X holds
( L is Lipschitzian iff ex K being Real st
( K > 0 & ( for x being Point of X holds abs (L . x) <= K * ||.x.|| ) ) );

definition
let X be RealUnitarySpace;
let Y be Subset of X;
attrY is weakly_summable_set  means :Def5: :: BHSP_6:def 5
 ex x being Point of X st
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (L . (x - (setsum Y1))) < e ) );
end;

:: deftheorem Def5 defines weakly_summable_set BHSP_6:def_5_:_
 for X being RealUnitarySpace
for Y being Subset of X holds
( Y is weakly_summable_set iff ex x being Point of X st
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (L . (x - (setsum Y1))) < e ) ) );

definition
let X be RealUnitarySpace;
let Y be Subset of X;
let L be Functional of X;
predY is_summable_set_by L means :Def6: :: BHSP_6:def 6
 ex r being Real st
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) );
end;

:: deftheorem Def6 defines is_summable_set_by BHSP_6:def_6_:_
 for X being RealUnitarySpace
for Y being Subset of X
for L being Functional of X holds
( Y is_summable_set_by L iff ex r being Real st
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) );

definition
let X be RealUnitarySpace;
let Y be Subset of X;
let L be Functional of X;
assume A1: Y is_summable_set_by L ;
func sum_byfunc (Y,L) ->  Real means :: BHSP_6:def 7
 for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (it - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) );
existence
 ex b1 being Real st
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (b1 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) by A1, Def6;
uniqueness
 for b1, b2 being Real st ( for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (b1 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) ) & ( for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (b2 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) ) holds
b1 = b2
proof
let r1, r2 be Real; ::_thesis: ( ( for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r1 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) ) & ( for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r2 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) ) implies r1 = r2 )
assume that
A2: for e1 being Real st e1 > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r1 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e1 ) ) and
A3: for e2 being Real st e2 > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r2 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e2 ) ) ; ::_thesis: r1 = r2
A4: now__::_thesis:_for_e3_being_real_number_st_e3_>_0_holds_
abs_(r1_-_r2)_<_e3
let e3 be real number ; ::_thesis: ( e3 > 0 implies abs (r1 - r2) < e3 )
assume A5: e3 > 0 ; ::_thesis: abs (r1 - r2) < e3
set e4 = e3 / 2;
consider Y01 being finite Subset of X such that
 not Y01 is empty and
A6: Y01 c= Y and
A7: for Y1 being finite Subset of X st Y01 c= Y1 & Y1 c= Y holds
abs (r1 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e3 / 2 by A2, A5, XREAL_1:139;
consider Y02 being finite Subset of X such that
 not Y02 is empty and
A8: Y02 c= Y and
A9: for Y1 being finite Subset of X st Y02 c= Y1 & Y1 c= Y holds
abs (r2 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e3 / 2 by A3, A5, XREAL_1:139;
set Y00 = Y01 \/ Y02;
A10: ( (e3 / 2) + (e3 / 2) = e3 & Y01 c= Y01 \/ Y02 ) by XBOOLE_1:7;
A11: Y01 \/ Y02 c= Y by A6, A8, XBOOLE_1:8;
then  abs (r2 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal))) < e3 / 2 by A9, XBOOLE_1:7;
then  ( abs ((r1 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal))) - (r2 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal)))) <= (abs (r1 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal)))) + (abs (r2 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal)))) & (abs (r1 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal)))) + (abs (r2 - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,L,addreal)))) < e3 ) by A7, A11, A10, COMPLEX1:57, XREAL_1:8;
hence  abs (r1 - r2) < e3 by XXREAL_0:2; ::_thesis: verum
end;
 r1 = r2
proof
assume A12: r1 <> r2 ; ::_thesis: contradiction
A13: abs (r1 - r2) <> 0
proof
assume  abs (r1 - r2) = 0 ; ::_thesis: contradiction
then  r1 - r2 = 0 by ABSVALUE:2;
hence  contradiction by A12; ::_thesis: verum
end;
 0 <= abs (r1 - r2) by COMPLEX1:46;
hence  contradiction by A4, A13; ::_thesis: verum
end;
hence  r1 = r2 ; ::_thesis: verum
end;
end;

:: deftheorem  defines sum_byfunc BHSP_6:def_7_:_
 for X being RealUnitarySpace
for Y being Subset of X
for L being Functional of X st Y is_summable_set_by L holds
for b4 being Real holds
( b4 = sum_byfunc (Y,L) iff for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (b4 - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) );

theorem Th3: :: BHSP_6:3
for X being RealUnitarySpace
for Y being Subset of X st Y is summable_set holds
Y is weakly_summable_set
proof
let X be RealUnitarySpace; ::_thesis: for Y being Subset of X st Y is summable_set holds
Y is weakly_summable_set
let Y be Subset of X; ::_thesis: ( Y is summable_set implies Y is weakly_summable_set )
assume  Y is summable_set ; ::_thesis: Y is weakly_summable_set
then consider x being Point of X such that
A1: for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e ) ) by Def2;
now__::_thesis:_for_L_being_linear-Functional_of_X_st_L_is_Lipschitzian_holds_
for_e1_being_Real_st_0_<_e1_holds_
ex_Y0_being_finite_Subset_of_X_st_
(_not_Y0_is_empty_&_Y0_c=_Y_&_(_for_Y1_being_finite_Subset_of_X_st_Y0_c=_Y1_&_Y1_c=_Y_holds_
abs_(L_._(x_-_(setsum_Y1)))_<_e1_)_)
let L be linear-Functional of X; ::_thesis: ( L is Lipschitzian implies for e1 being Real st 0 < e1 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (L . (x - (setsum Y1))) < e1 ) ) )
assume  L is Lipschitzian ; ::_thesis: for e1 being Real st 0 < e1 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (L . (x - (setsum Y1))) < e1 ) )
then consider K being Real such that
A2: 0 < K and
A3: for x being Point of X holds abs (L . x) <= K * ||.x.|| by Def4;
now__::_thesis:_for_e1_being_Real_st_0_<_e1_holds_
ex_Y0_being_finite_Subset_of_X_st_
(_not_Y0_is_empty_&_Y0_c=_Y_&_(_for_Y1_being_finite_Subset_of_X_st_Y0_c=_Y1_&_Y1_c=_Y_holds_
abs_(L_._(x_-_(setsum_Y1)))_<_e1_)_)
let e1 be Real; ::_thesis: ( 0 < e1 implies ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (L . (x - (setsum Y1))) < e1 ) ) )
assume A4: 0 < e1 ; ::_thesis: ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (L . (x - (setsum Y1))) < e1 ) )
set e = e1 / K;
consider Y0 being finite Subset of X such that
A5: ( not Y0 is empty & Y0 c= Y ) and
A6: for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e1 / K by A1, A2, A4, XREAL_1:139;
A7: (e1 / K) * K = e1 by A2, XCMPLX_1:87;
now__::_thesis:_for_Y1_being_finite_Subset_of_X_st_Y0_c=_Y1_&_Y1_c=_Y_holds_
abs_(L_._(x_-_(setsum_Y1)))_<_e1
let Y1 be finite Subset of X; ::_thesis: ( Y0 c= Y1 & Y1 c= Y implies abs (L . (x - (setsum Y1))) < e1 )
assume  ( Y0 c= Y1 & Y1 c= Y ) ; ::_thesis: abs (L . (x - (setsum Y1))) < e1
then  K * ||.(x - (setsum Y1)).|| < e1 by A2, A7, A6, XREAL_1:68;
then  (abs (L . (x - (setsum Y1)))) + (K * ||.(x - (setsum Y1)).||) < (K * ||.(x - (setsum Y1)).||) + e1 by A3, XREAL_1:8;
then  ((abs (L . (x - (setsum Y1)))) + (K * ||.(x - (setsum Y1)).||)) - (K * ||.(x - (setsum Y1)).||) < ((K * ||.(x - (setsum Y1)).||) + e1) - (K * ||.(x - (setsum Y1)).||) by XREAL_1:14;
hence  abs (L . (x - (setsum Y1))) < e1 ; ::_thesis: verum
end;
hence  ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (L . (x - (setsum Y1))) < e1 ) ) by A5; ::_thesis: verum
end;
hence  for e1 being Real st 0 < e1 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (L . (x - (setsum Y1))) < e1 ) ) ; ::_thesis: verum
end;
hence  Y is weakly_summable_set by Def5; ::_thesis: verum
end;

theorem Th4: :: BHSP_6:4
for X being RealUnitarySpace
for L being linear-Functional of X
for p being FinSequence of the carrier of X st len p >= 1 holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = L . (p . i) ) holds
L . ( the addF of X "**" p) = addreal "**" q
proof
let X be RealUnitarySpace; ::_thesis: for L being linear-Functional of X
for p being FinSequence of the carrier of X st len p >= 1 holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = L . (p . i) ) holds
L . ( the addF of X "**" p) = addreal "**" q
let L be linear-Functional of X; ::_thesis: for p being FinSequence of the carrier of X st len p >= 1 holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = L . (p . i) ) holds
L . ( the addF of X "**" p) = addreal "**" q
let p be FinSequence of the carrier of X; ::_thesis: ( len p >= 1 implies for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = L . (p . i) ) holds
L . ( the addF of X "**" p) = addreal "**" q )
assume A1: len p >= 1 ; ::_thesis: for q being FinSequence of REAL st dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = L . (p . i) ) holds
L . ( the addF of X "**" p) = addreal "**" q
consider f being Function of NAT, the carrier of X such that
A2: f . 1 = p . 1 and
A3: for n being Element of NAT st 0 <> n & n < len p holds
f . (n + 1) = the addF of X . ((f . n),(p . (n + 1))) and
A4: the addF of X "**" p = f . (len p) by A1, FINSOP_1:1;
let q be FinSequence of REAL ; ::_thesis: ( dom p = dom q & ( for i being Element of NAT st i in dom q holds
q . i = L . (p . i) ) implies L . ( the addF of X "**" p) = addreal "**" q )
assume that
A5: dom p = dom q and
A6: for i being Element of NAT st i in dom q holds
q . i = L . (p . i) ; ::_thesis: L . ( the addF of X "**" p) = addreal "**" q
Seg (len q) = dom p by A5, FINSEQ_1:def_3
.= Seg (len p) by FINSEQ_1:def_3 ;
then A7: len q = len p by FINSEQ_1:6;
then consider g being Function of NAT,REAL such that
A8: g . 1 = q . 1 and
A9: for n being Element of NAT st 0 <> n & n < len q holds
g . (n + 1) = addreal . ((g . n),(q . (n + 1))) and
A10: addreal "**" q = g . (len q) by A1, FINSOP_1:1;
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len q implies g . $1 = L . (f . $1) );
A11: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A12: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_(_1_<=_n_+_1_&_n_+_1_<=_len_q_implies_g_._(n_+_1)_=_L_._(f_._(n_+_1))_)
A13: n <= n + 1 by NAT_1:11;
assume that
A14: 1 <= n + 1 and
A15: n + 1 <= len q ; ::_thesis: g . (n + 1) = L . (f . (n + 1))
percases ( n = 0 or n <> 0 ) ;
supposeA16: n = 0 ; ::_thesis: g . (n + 1) = L . (f . (n + 1))
 1 in dom p by A1, FINSEQ_3:25;
hence  g . (n + 1) = L . (f . (n + 1)) by A5, A6, A2, A8, A16; ::_thesis: verum
end;
supposeA17: n <> 0 ; ::_thesis: g . (n + 1) = L . (f . (n + 1))
then A18: 0 + 1 <= n by INT_1:7;
reconsider z = f . n as Element of X ;
reconsider z1 = z as VECTOR of X ;
A19: n + 1 in dom q by A14, A15, FINSEQ_3:25;
then  p . (n + 1) in rng p by A5, FUNCT_1:3;
then reconsider y = p . (n + 1) as Element of X ;
reconsider y1 = y as VECTOR of X ;
set Lz = L . z1;
set Ly = L . y1;
A20: (n + 1) - 1 < (len q) - 0 by A15, XREAL_1:15;
hence g . (n + 1) = addreal . ((g . n),(q . (n + 1))) by A9, A17
.= addreal . ((L . (f . n)),(L . y)) by A6, A12, A15, A13, A18, A19, XXREAL_0:2
.= (L . z1) + (L . y1) by BINOP_2:def_9
.= L . (z1 + y1) by HAHNBAN:def_2
.= L . (f . (n + 1)) by A3, A7, A17, A20 ;
::_thesis: verum
end;
end;
end;
hence  S1[n + 1] ; ::_thesis: verum
end;
A21: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A21, A11);
hence  L . ( the addF of X "**" p) = addreal "**" q by A1, A4, A7, A10; ::_thesis: verum
end;

theorem Th5: :: BHSP_6:5
for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for S being finite Subset of X st not S is empty holds
for L being linear-Functional of X holds L . (setsum S) = setopfunc (S, the carrier of X,REAL,L,addreal)
proof
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 S being finite Subset of X st not S is empty holds
for L being linear-Functional of X holds L . (setsum S) = setopfunc (S, the carrier of X,REAL,L,addreal) )
assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity ) ; ::_thesis: for S being finite Subset of X st not S is empty holds
for L being linear-Functional of X holds L . (setsum S) = setopfunc (S, the carrier of X,REAL,L,addreal)
let S be finite Subset of X; ::_thesis: ( not S is empty implies for L being linear-Functional of X holds L . (setsum S) = setopfunc (S, the carrier of X,REAL,L,addreal) )
assume  not S is empty ; ::_thesis: for L being linear-Functional of X holds L . (setsum S) = setopfunc (S, the carrier of X,REAL,L,addreal)
then A2: 0 + 1 <= card S by INT_1:7;
let L be linear-Functional of X; ::_thesis: L . (setsum S) = setopfunc (S, the carrier of X,REAL,L,addreal)
consider p being FinSequence of the carrier of X such that
A3: ( p is one-to-one & rng p = S ) and
A4: setsum S = the addF of X "**" p by A1, Def1;
reconsider q1 = Func_Seq (L,p) as FinSequence of REAL ;
A5: for i being Element of NAT st i in dom p holds
q1 . i = L . (p . i)
proof
let i be Element of NAT ; ::_thesis: ( i in dom p implies q1 . i = L . (p . i) )
assume A6: i in dom p ; ::_thesis: q1 . i = L . (p . i)
q1 . i = (L * p) . i by BHSP_5:def_4
.= L . (p . i) by A6, FUNCT_1:13 ;
hence  q1 . i = L . (p . i) ; ::_thesis: verum
end;
A7: dom L = the carrier of X by FUNCT_2:def_1;
now__::_thesis:_for_xd_being_set_holds_
(_xd_in_dom_(Func_Seq_(L,p))_iff_xd_in_dom_p_)
let xd be set ; ::_thesis: ( xd in dom (Func_Seq (L,p)) iff xd in dom p )
A8: ( xd in dom p implies p . xd in rng p ) by FUNCT_1:3;
 ( xd in dom (Func_Seq (L,p)) iff xd in dom (L * p) ) by BHSP_5:def_4;
hence  ( xd in dom (Func_Seq (L,p)) iff xd in dom p ) by A7, A8, FUNCT_1:11; ::_thesis: verum
end;
then A9: dom (Func_Seq (L,p)) = dom p by TARSKI:1;
 len p >= 1 by A3, A2, FINSEQ_4:62;
then  L . ( the addF of X "**" p) = addreal "**" q1 by A9, A5, Th4;
hence  L . (setsum S) = setopfunc (S, the carrier of X,REAL,L,addreal) by A7, A3, A4, BHSP_5:def_5; ::_thesis: verum
end;

theorem Th6: :: BHSP_6:6
for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for Y being Subset of X st Y is weakly_summable_set holds
ex x being Point of X st
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) )
proof
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 Subset of X st Y is weakly_summable_set holds
ex x being Point of X st
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) )
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 Subset of X st Y is weakly_summable_set holds
ex x being Point of X st
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) )
let Y be Subset of X; ::_thesis: ( Y is weakly_summable_set implies ex x being Point of X st
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) )
assume  Y is weakly_summable_set ; ::_thesis: ex x being Point of X st
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) )
then consider x being Point of X such that
A2: for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (L . (x - (setsum Y1))) < e ) ) by Def5;
take  x ; ::_thesis: for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) )
now__::_thesis:_for_L_being_linear-Functional_of_X_st_L_is_Lipschitzian_holds_
for_e_being_Real_st_e_>_0_holds_
ex_Y0_being_finite_Subset_of_X_st_
(_not_Y0_is_empty_&_Y0_c=_Y_&_(_for_Y1_being_finite_Subset_of_X_st_Y0_c=_Y1_&_Y1_c=_Y_holds_
abs_((L_._x)_-_(setopfunc_(Y1,_the_carrier_of_X,REAL,L,addreal)))_<_e_)_)
let L be linear-Functional of X; ::_thesis: ( L is Lipschitzian implies for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) )
assume A3: L is Lipschitzian ; ::_thesis: for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) )
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_Y0_being_finite_Subset_of_X_st_
(_not_Y0_is_empty_&_Y0_c=_Y_&_(_for_Y1_being_finite_Subset_of_X_st_Y0_c=_Y1_&_Y1_c=_Y_holds_
abs_((L_._x)_-_(setopfunc_(Y1,_the_carrier_of_X,REAL,L,addreal)))_<_e_)_)
let e be Real; ::_thesis: ( e > 0 implies ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) )
assume  e > 0 ; ::_thesis: ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) )
then consider Y0 being finite Subset of X such that
A4: not Y0 is empty and
A5: Y0 c= Y and
A6: for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (L . (x - (setsum Y1))) < e by A2, A3;
take Y0 = Y0; ::_thesis: ( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) )
now__::_thesis:_for_Y1_being_finite_Subset_of_X_st_Y0_c=_Y1_&_Y1_c=_Y_holds_
abs_((L_._x)_-_(setopfunc_(Y1,_the_carrier_of_X,REAL,L,addreal)))_<_e
set x1 = x;
let Y1 be finite Subset of X; ::_thesis: ( Y0 c= Y1 & Y1 c= Y implies abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e )
assume that
A7: Y0 c= Y1 and
A8: Y1 c= Y ; ::_thesis: abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e
set y1 = setsum Y1;
set r = L . (x - (setsum Y1));
 Y1 <> {} by A4, A7;
then  ( L . (x - (setsum Y1)) = (L . x) - (L . (setsum Y1)) & L . (setsum Y1) = setopfunc (Y1, the carrier of X,REAL,L,addreal) ) by A1, Th5, HAHNBAN:19;
hence  abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e by A6, A7, A8; ::_thesis: verum
end;
hence  ( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) by A4, A5; ::_thesis: verum
end;
hence  for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) ; ::_thesis: verum
end;
hence  for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) ; ::_thesis: verum
end;

theorem Th7: :: BHSP_6:7
for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for Y being Subset of X st Y is weakly_summable_set holds
for L being linear-Functional of X st L is Lipschitzian holds
Y is_summable_set_by L
proof
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 Subset of X st Y is weakly_summable_set holds
for L being linear-Functional of X st L is Lipschitzian holds
Y is_summable_set_by L )
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 Subset of X st Y is weakly_summable_set holds
for L being linear-Functional of X st L is Lipschitzian holds
Y is_summable_set_by L
let Y be Subset of X; ::_thesis: ( Y is weakly_summable_set implies for L being linear-Functional of X st L is Lipschitzian holds
Y is_summable_set_by L )
assume  Y is weakly_summable_set ; ::_thesis: for L being linear-Functional of X st L is Lipschitzian holds
Y is_summable_set_by L
then consider x being Point of X such that
A2: for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) by A1, Th6;
let L be linear-Functional of X; ::_thesis: ( L is Lipschitzian implies Y is_summable_set_by L )
assume  L is Lipschitzian ; ::_thesis: Y is_summable_set_by L
then  for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs ((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) by A2;
hence  Y is_summable_set_by L by Def6; ::_thesis: verum
end;

theorem :: BHSP_6:8
for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for Y being Subset of X st Y is summable_set holds
for L being linear-Functional of X st L is Lipschitzian holds
Y is_summable_set_by L by Th3, Th7;

theorem :: BHSP_6:9
for X being RealUnitarySpace
for Y being finite Subset of X st not Y is empty holds
Y is summable_set
proof
let X be RealUnitarySpace; ::_thesis: for Y being finite Subset of X st not Y is empty holds
Y is summable_set
let Y be finite Subset of X; ::_thesis: ( not Y is empty implies Y is summable_set )
assume A1: not Y is empty ; ::_thesis: Y is summable_set
set x = setsum Y;
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_Y0_being_finite_Subset_of_X_st_
(_not_Y0_is_empty_&_Y0_c=_Y_&_(_for_Y1_being_finite_Subset_of_X_st_Y0_c=_Y1_&_Y1_c=_Y_holds_
||.((setsum_Y)_-_(setsum_Y1)).||_<_e_)_)
let e be Real; ::_thesis: ( e > 0 implies ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.((setsum Y) - (setsum Y1)).|| < e ) ) )
assume A2: e > 0 ; ::_thesis: ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.((setsum Y) - (setsum Y1)).|| < e ) )
 ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.((setsum Y) - (setsum Y1)).|| < e ) )
proof
take  Y ; ::_thesis: ( not Y is empty & Y c= Y & ( for Y1 being finite Subset of X st Y c= Y1 & Y1 c= Y holds
||.((setsum Y) - (setsum Y1)).|| < e ) )
now__::_thesis:_for_Y1_being_finite_Subset_of_X_st_Y_c=_Y1_&_Y1_c=_Y_holds_
||.((setsum_Y)_-_(setsum_Y1)).||_<_e
let Y1 be finite Subset of X; ::_thesis: ( Y c= Y1 & Y1 c= Y implies ||.((setsum Y) - (setsum Y1)).|| < e )
assume  ( Y c= Y1 & Y1 c= Y ) ; ::_thesis: ||.((setsum Y) - (setsum Y1)).|| < e
then  Y1 = Y by XBOOLE_0:def_10;
then  (setsum Y) - (setsum Y1) = 0. X by RLVECT_1:15;
hence  ||.((setsum Y) - (setsum Y1)).|| < e by A2, BHSP_1:26; ::_thesis: verum
end;
hence  ( not Y is empty & Y c= Y & ( for Y1 being finite Subset of X st Y c= Y1 & Y1 c= Y holds
||.((setsum Y) - (setsum Y1)).|| < e ) ) by A1; ::_thesis: verum
end;
hence  ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.((setsum Y) - (setsum Y1)).|| < e ) ) ; ::_thesis: verum
end;
hence  Y is summable_set by Def2; ::_thesis: verum
end;

begin

theorem :: BHSP_6:10
for X being RealHilbertSpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for Y being Subset of X holds
( Y is summable_set iff for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) )
proof
let X be RealHilbertSpace; ::_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 Subset of X holds
( Y is summable_set iff for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) ) )
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 Subset of X holds
( Y is summable_set iff for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) )
let Y be Subset of X; ::_thesis: ( Y is summable_set iff for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) )
A2: now__::_thesis:_(_(_for_e_being_Real_st_e_>_0_holds_
ex_Y0_being_finite_Subset_of_X_st_
(_not_Y0_is_empty_&_Y0_c=_Y_&_(_for_Y1_being_finite_Subset_of_X_st_not_Y1_is_empty_&_Y1_c=_Y_&_Y0_misses_Y1_holds_
||.(setsum_Y1).||_<_e_)_)_)_implies_Y_is_summable_set_)
defpred S1[ set , set ] means ( $2 is finite Subset of X & not $2 is empty & $2 c= Y & ( for z being Real st z = $1 holds
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & $2 misses Y1 holds
||.(setsum Y1).|| < 1 / (z + 1) ) );
assume A3: for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) ; ::_thesis: Y is summable_set
A4: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
ex_y_being_set_st_
(_y_in_bool_Y_&_S1[x,y]_)
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in bool Y & S1[x,y] ) )
assume  x in NAT ; ::_thesis: ex y being set st
( y in bool Y & S1[x,y] )
then reconsider xx = x as Element of NAT ;
reconsider e = 1 / (xx + 1) as Real by XREAL_0:def_1;
 0 / (xx + 1) < 1 / (xx + 1) by XREAL_1:74;
then consider Y0 being finite Subset of X such that
A5: ( not Y0 is empty & Y0 c= Y ) and
A6: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e by A3;
 for z being Real st z = x holds
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < 1 / (z + 1) by A6;
hence  ex y being set st
( y in bool Y & S1[x,y] ) by A5; ::_thesis: verum
end;
A7: ex B being Function of NAT,(bool Y) st
for x being set st x in NAT holds
S1[x,B . x] from FUNCT_2:sch_1(A4);
 ex A being Function of NAT,(bool Y) st
for i being Element of NAT holds
( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds
||.(setsum Y1).|| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds
A . i c= A . j ) )
proof
consider B being Function of NAT,(bool Y) such that
A8: for x being set st x in NAT holds
( B . x is finite Subset of X & not B . x is empty & B . x c= Y & ( for z being Real st z = x holds
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & B . x misses Y1 holds
||.(setsum Y1).|| < 1 / (z + 1) ) ) by A7;
deffunc H1( Nat, set ) ->  set = (B . ($1 + 1)) \/ $2;
 ex A being Function st
( dom A = NAT & A . 0 = B . 0 & ( for n being Nat holds A . (n + 1) = H1(n,A . n) ) ) from NAT_1:sch_11();
then consider A being Function such that
A9: dom A = NAT and
A10: A . 0 = B . 0 and
A11: for n being Nat holds A . (n + 1) = (B . (n + 1)) \/ (A . n) ;
defpred S2[ Element of NAT ] means ( A . $1 is finite Subset of X & not A . $1 is empty & A . $1 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . $1 misses Y1 holds
||.(setsum Y1).|| < 1 / ($1 + 1) ) & ( for j being Element of NAT st $1 <= j holds
A . $1 c= A . j ) );
A12: now__::_thesis:_for_n_being_Element_of_NAT_st_S2[n]_holds_
S2[n_+_1]
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A13: S2[n] ; ::_thesis: S2[n + 1]
A14: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . (n + 1) misses Y1 holds
||.(setsum Y1).|| < 1 / ((n + 1) + 1)
proof
let Y1 be finite Subset of X; ::_thesis: ( not Y1 is empty & Y1 c= Y & A . (n + 1) misses Y1 implies ||.(setsum Y1).|| < 1 / ((n + 1) + 1) )
assume that
A15: ( not Y1 is empty & Y1 c= Y ) and
A16: A . (n + 1) misses Y1 ; ::_thesis: ||.(setsum Y1).|| < 1 / ((n + 1) + 1)
 A . (n + 1) = (B . (n + 1)) \/ (A . n) by A11;
then  B . (n + 1) misses Y1 by A16, XBOOLE_1:7, XBOOLE_1:63;
hence  ||.(setsum Y1).|| < 1 / ((n + 1) + 1) by A8, A15; ::_thesis: verum
end;
defpred S3[ Element of NAT ] means ( n + 1 <= $1 implies A . (n + 1) c= A . $1 );
A17: for j being Element of NAT st S3[j] holds
S3[j + 1]
proof
let j be Element of NAT ; ::_thesis: ( S3[j] implies S3[j + 1] )
assume that
A18: ( n + 1 <= j implies A . (n + 1) c= A . j ) and
A19: n + 1 <= j + 1 ; ::_thesis: A . (n + 1) c= A . (j + 1)
percases ( n = j or n <> j ) ;
suppose n = j ; ::_thesis: A . (n + 1) c= A . (j + 1)
hence  A . (n + 1) c= A . (j + 1) ; ::_thesis: verum
end;
supposeA20: n <> j ; ::_thesis: A . (n + 1) c= A . (j + 1)
 A . (j + 1) = (B . (j + 1)) \/ (A . j) by A11;
then A21: A . j c= A . (j + 1) by XBOOLE_1:7;
 n <= j by A19, XREAL_1:6;
then  n < j by A20, XXREAL_0:1;
hence  A . (n + 1) c= A . (j + 1) by A18, A21, NAT_1:13, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
A22: S3[ 0 ] ;
A23: for j being Element of NAT holds S3[j] from NAT_1:sch_1(A22, A17);
 ( A . (n + 1) = (B . (n + 1)) \/ (A . n) & B . (n + 1) is finite Subset of X ) by A8, A11;
hence  S2[n + 1] by A13, A14, A23, XBOOLE_1:8; ::_thesis: verum
end;
 for j0 being Element of NAT st j0 = 0 holds
for j being Element of NAT st j0 <= j holds
A . j0 c= A . j
proof
let j0 be Element of NAT ; ::_thesis: ( j0 = 0 implies for j being Element of NAT st j0 <= j holds
A . j0 c= A . j )
assume A24: j0 = 0 ; ::_thesis: for j being Element of NAT st j0 <= j holds
A . j0 c= A . j
defpred S3[ Element of NAT ] means ( j0 <= $1 implies A . j0 c= A . $1 );
A25: now__::_thesis:_for_j_being_Element_of_NAT_st_S3[j]_holds_
S3[j_+_1]
let j be Element of NAT ; ::_thesis: ( S3[j] implies S3[j + 1] )
assume A26: S3[j] ; ::_thesis: S3[j + 1]
 A . (j + 1) = (B . (j + 1)) \/ (A . j) by A11;
then  A . j c= A . (j + 1) by XBOOLE_1:7;
hence  S3[j + 1] by A24, A26, XBOOLE_1:1; ::_thesis: verum
end;
A27: S3[ 0 ] ;
thus  for j being Element of NAT holds S3[j] from NAT_1:sch_1(A27, A25); ::_thesis: verum
end;
then A28: S2[ 0 ] by A8, A10;
A29: for i being Element of NAT holds S2[i] from NAT_1:sch_1(A28, A12);
now__::_thesis:_for_y_being_set_st_y_in_rng_A_holds_
y_in_bool_Y
let y be set ; ::_thesis: ( y in rng A implies y in bool Y )
assume  y in rng A ; ::_thesis: y in bool Y
then consider x being set  such that
A30: x in dom A and
A31: y = A . x by FUNCT_1:def_3;
reconsider i = x as Element of NAT by A9, A30;
 A . i c= Y by A29;
hence  y in bool Y by A31; ::_thesis: verum
end;
then  rng A c= bool Y by TARSKI:def_3;
then  A is Function of NAT,(bool Y) by A9, FUNCT_2:2;
hence  ex A being Function of NAT,(bool Y) st
for i being Element of NAT holds
( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds
||.(setsum Y1).|| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds
A . i c= A . j ) ) by A29; ::_thesis: verum
end;
then consider A being Function of NAT,(bool Y) such that
A32: for i being Element of NAT holds
( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds
||.(setsum Y1).|| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds
A . i c= A . j ) ) ;
defpred S2[ set , set ] means  ex Y1 being finite Subset of X st
( not Y1 is empty & A . $1 = Y1 & $2 = setsum Y1 );
A33: for x being set st x in NAT holds
ex y being set st
( y in the carrier of X & S2[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in the carrier of X & S2[x,y] ) )
assume  x in NAT ; ::_thesis: ex y being set st
( y in the carrier of X & S2[x,y] )
then reconsider i = x as Element of NAT ;
 A . i is finite Subset of X by A32;
then reconsider Y1 = A . x as finite Subset of X ;
reconsider y = setsum Y1 as set ;
 not A . i is empty by A32;
then  ex Y1 being finite Subset of X st
( Y1 is non empty set & A . x = Y1 & y = setsum Y1 ) ;
hence  ex y being set st
( y in the carrier of X & S2[x,y] ) ; ::_thesis: verum
end;
 ex F being Function of NAT, the carrier of X st
for x being set st x in NAT holds
S2[x,F . x] from FUNCT_2:sch_1(A33);
then consider F being Function of NAT, the carrier of X such that
A34: for x being set st x in NAT holds
ex Y1 being finite Subset of X st
( not Y1 is empty & A . x = Y1 & F . x = setsum Y1 ) ;
reconsider seq = F as sequence of X ;
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((seq_._n)_-_(seq_._m)).||_<_e
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < e )
assume A35: e > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < e
A36: e / 2 > 0 / 2 by A35, XREAL_1:74;
 ex k being Element of NAT st 1 / (k + 1) < e / 2
proof
set p = e / 2;
consider k1 being Element of NAT  such that
A37: (e / 2) " < k1 by SEQ_4:3;
take k = k1; ::_thesis: 1 / (k + 1) < e / 2
 ((e / 2) ") + 0 < k1 + 1 by A37, XREAL_1:8;
then  1 / (k1 + 1) < 1 / ((e / 2) ") by A36, XREAL_1:76;
then  1 / (k + 1) < 1 * (((e / 2) ") ") by XCMPLX_0:def_9;
hence  1 / (k + 1) < e / 2 ; ::_thesis: verum
end;
then consider k being Element of NAT  such that
A38: 1 / (k + 1) < e / 2 ;
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((seq_._n)_-_(seq_._m)).||_<_e
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((seq . n) - (seq . m)).|| < e )
assume that
A39: n >= k and
A40: m >= k ; ::_thesis: ||.((seq . n) - (seq . m)).|| < e
consider Y2 being finite Subset of X such that
 not Y2 is empty and
A41: A . m = Y2 and
A42: seq . m = setsum Y2 by A34;
consider Y0 being finite Subset of X such that
 not Y0 is empty and
A43: A . k = Y0 and
A44: seq . k = setsum Y0 by A34;
A45: Y0 c= Y2 by A32, A40, A43, A41;
consider Y1 being finite Subset of X such that
 not Y1 is empty and
A46: A . n = Y1 and
A47: seq . n = setsum Y1 by A34;
A48: Y0 c= Y1 by A32, A39, A43, A46;
now__::_thesis:_(_(_Y0_=_Y1_&_||.((seq_._n)_-_(seq_._m)).||_<_e_)_or_(_Y0_<>_Y1_&_||.((seq_._n)_-_(seq_._m)).||_<_e_)_)
percases ( Y0 = Y1 or Y0 <> Y1 ) ;
caseA49: Y0 = Y1 ; ::_thesis: ||.((seq . n) - (seq . m)).|| < e
now__::_thesis:_(_(_Y0_=_Y2_&_||.((seq_._n)_-_(seq_._m)).||_<_e_)_or_(_Y0_<>_Y2_&_||.((seq_._n)_-_(seq_._m)).||_<_e_)_)
percases ( Y0 = Y2 or Y0 <> Y2 ) ;
case Y0 = Y2 ; ::_thesis: ||.((seq . n) - (seq . m)).|| < e
then  (seq . n) - (seq . m) = 0. X by A47, A42, A49, RLVECT_1:5;
hence  ||.((seq . n) - (seq . m)).|| < e by A35, BHSP_1:26; ::_thesis: verum
end;
caseA50: Y0 <> Y2 ; ::_thesis: ||.((seq . n) - (seq . m)).|| < e
 ex Y02 being finite Subset of X st
( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )
proof
take Y02 = Y2 \ Y0; ::_thesis: ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )
A51: Y2 \ Y0 c= Y2 by XBOOLE_1:36;
Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
.= Y2 by A45, XBOOLE_1:12 ;
hence  ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A41, A50, A51, XBOOLE_1:1, XBOOLE_1:79; ::_thesis: verum
end;
then consider Y02 being finite Subset of X such that
A52: ( not Y02 is empty & Y02 c= Y ) and
A53: Y02 misses Y0 and
A54: Y0 \/ Y02 = Y2 ;
 ||.(setsum Y02).|| < 1 / (k + 1) by A32, A43, A52, A53;
then A55: ||.(setsum Y02).|| < e / 2 by A38, XXREAL_0:2;
 setsum Y2 = (setsum Y0) + (setsum Y02) by A1, A53, A54, Th2;
then A56: ||.((seq . n) - (seq . m)).|| = ||.(((setsum Y0) - (setsum Y0)) - (setsum Y02)).|| by A47, A42, A49, RLVECT_1:27
.= ||.((0. X) - (setsum Y02)).|| by RLVECT_1:15
.= ||.(- (setsum Y02)).|| by RLVECT_1:14
.= ||.(setsum Y02).|| by BHSP_1:31 ;
 e * (1 / 2) < e * 1 by A35, XREAL_1:68;
hence  ||.((seq . n) - (seq . m)).|| < e by A55, A56, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  ||.((seq . n) - (seq . m)).|| < e ; ::_thesis: verum
end;
caseA57: Y0 <> Y1 ; ::_thesis: ||.((seq . n) - (seq . m)).|| < e
now__::_thesis:_(_(_Y0_=_Y2_&_||.((seq_._n)_-_(seq_._m)).||_<_e_)_or_(_Y0_<>_Y2_&_||.((seq_._n)_-_(seq_._m)).||_<_e_)_)
percases ( Y0 = Y2 or Y0 <> Y2 ) ;
case Y0 = Y2 ; ::_thesis: ||.((seq . n) - (seq . m)).|| < e
then A58: (seq . k) - (seq . m) = 0. X by A44, A42, RLVECT_1:5;
 ex Y01 being finite Subset of X st
( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )
proof
take Y01 = Y1 \ Y0; ::_thesis: ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )
A59: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A48, XBOOLE_1:12 ;
hence  ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A46, A57, A59, XBOOLE_1:1, XBOOLE_1:79; ::_thesis: verum
end;
then consider Y01 being finite Subset of X such that
A60: ( not Y01 is empty & Y01 c= Y ) and
A61: Y01 misses Y0 and
A62: Y0 \/ Y01 = Y1 ;
 seq . n = (seq . k) + (setsum Y01) by A1, A44, A47, A61, A62, Th2;
then A63: (seq . n) - (seq . k) = (seq . k) + ((setsum Y01) + (- (seq . k))) by RLVECT_1:def_3
.= (seq . k) - ((seq . k) - (setsum Y01)) by RLVECT_1:33
.= ((setsum Y0) - (setsum Y0)) + (setsum Y01) by A44, RLVECT_1:29
.= (0. X) + (setsum Y01) by RLVECT_1:5
.= setsum Y01 by RLVECT_1:4 ;
(seq . n) - (seq . m) = ((seq . n) - (seq . m)) + (0. X) by RLVECT_1:4
.= ((seq . n) - (seq . m)) + ((seq . k) - (seq . k)) by RLVECT_1:5
.= (seq . n) - ((seq . m) - ((seq . k) - (seq . k))) by RLVECT_1:29
.= (seq . n) - (((seq . m) - (seq . k)) + (seq . k)) by RLVECT_1:29
.= (seq . n) - ((seq . k) - ((seq . k) - (seq . m))) by RLVECT_1:33
.= (setsum Y01) + (0. X) by A63, A58, RLVECT_1:29 ;
then  ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(0. X).|| by BHSP_1:30;
then A64: ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + 0 by BHSP_1:26;
 ||.(setsum Y01).|| < 1 / (k + 1) by A32, A43, A60, A61;
then  ||.(setsum Y01).|| < e / 2 by A38, XXREAL_0:2;
then  ||.((seq . n) - (seq . m)).|| < e / 2 by A64, XXREAL_0:2;
then  ||.((seq . n) - (seq . m)).|| + 0 < (e / 2) + (e / 2) by A35, XREAL_1:8;
hence  ||.((seq . n) - (seq . m)).|| < e ; ::_thesis: verum
end;
caseA65: Y0 <> Y2 ; ::_thesis: ||.((seq . n) - (seq . m)).|| < e
 ex Y02 being finite Subset of X st
( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )
proof
take Y02 = Y2 \ Y0; ::_thesis: ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )
A66: Y2 \ Y0 c= Y2 by XBOOLE_1:36;
Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
.= Y2 by A45, XBOOLE_1:12 ;
hence  ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A41, A65, A66, XBOOLE_1:1, XBOOLE_1:79; ::_thesis: verum
end;
then consider Y02 being finite Subset of X such that
A67: ( not Y02 is empty & Y02 c= Y ) and
A68: Y02 misses Y0 and
A69: Y0 \/ Y02 = Y2 ;
 ||.(setsum Y02).|| < 1 / (k + 1) by A32, A43, A67, A68;
then A70: ||.(setsum Y02).|| < e / 2 by A38, XXREAL_0:2;
 ex Y01 being finite Subset of X st
( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )
proof
take Y01 = Y1 \ Y0; ::_thesis: ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )
A71: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A48, XBOOLE_1:12 ;
hence  ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A46, A57, A71, XBOOLE_1:1, XBOOLE_1:79; ::_thesis: verum
end;
then consider Y01 being finite Subset of X such that
A72: ( not Y01 is empty & Y01 c= Y ) and
A73: Y01 misses Y0 and
A74: Y0 \/ Y01 = Y1 ;
 setsum Y1 = (setsum Y0) + (setsum Y01) by A1, A73, A74, Th2;
then A75: (seq . n) - (seq . k) = (setsum Y01) + ((seq . k) + (- (seq . k))) by A44, A47, RLVECT_1:def_3
.= (setsum Y01) + (0. X) by RLVECT_1:5
.= setsum Y01 by RLVECT_1:4 ;
 setsum Y2 = (setsum Y0) + (setsum Y02) by A1, A68, A69, Th2;
then A76: (seq . m) - (seq . k) = (setsum Y02) + ((seq . k) + (- (seq . k))) by A44, A42, RLVECT_1:def_3
.= (setsum Y02) + (0. X) by RLVECT_1:5
.= setsum Y02 by RLVECT_1:4 ;
(seq . n) - (seq . m) = ((seq . n) - (seq . m)) + (0. X) by RLVECT_1:4
.= ((seq . n) - (seq . m)) + ((seq . k) - (seq . k)) by RLVECT_1:5
.= (seq . n) - ((seq . m) - ((seq . k) - (seq . k))) by RLVECT_1:29
.= (seq . n) - (((seq . m) - (seq . k)) + (seq . k)) by RLVECT_1:29
.= (seq . n) - ((seq . k) - ((seq . k) - (seq . m))) by RLVECT_1:33
.= ((seq . n) - (seq . k)) + ((seq . k) + (- (seq . m))) by RLVECT_1:29
.= (setsum Y01) + (- (setsum Y02)) by A75, A76, RLVECT_1:33 ;
then  ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(- (setsum Y02)).|| by BHSP_1:30;
then A77: ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(setsum Y02).|| by BHSP_1:31;
 ||.(setsum Y01).|| < 1 / (k + 1) by A32, A43, A72, A73;
then  ||.(setsum Y01).|| < e / 2 by A38, XXREAL_0:2;
then  ||.(setsum Y01).|| + ||.(setsum Y02).|| < (e / 2) + (e / 2) by A70, XREAL_1:8;
hence  ||.((seq . n) - (seq . m)).|| < e by A77, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  ||.((seq . n) - (seq . m)).|| < e ; ::_thesis: verum
end;
end;
end;
hence  ||.((seq . n) - (seq . m)).|| < e ; ::_thesis: verum
end;
hence  ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < e ; ::_thesis: verum
end;
then  seq is Cauchy by BHSP_3:2;
then  seq is convergent by BHSP_3:def_4;
then consider x being Point of X such that
A78: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq . n) - x).|| < r by BHSP_2:9;
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_Y0_being_finite_Subset_of_X_st_
(_not_Y0_is_empty_&_Y0_c=_Y_&_(_for_Y1_being_finite_Subset_of_X_st_Y0_c=_Y1_&_Y1_c=_Y_holds_
||.(x_-_(setsum_Y1)).||_<_e_)_)
let e be Real; ::_thesis: ( e > 0 implies ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e ) ) )
assume A79: e > 0 ; ::_thesis: ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e ) )
A80: e / 2 > 0 / 2 by A79, XREAL_1:74;
then consider m being Element of NAT  such that
A81: for n being Element of NAT st n >= m holds
||.((seq . n) - x).|| < e / 2 by A78;
 ex i being Element of NAT st
( 1 / (i + 1) < e / 2 & i >= m )
proof
set p = e / 2;
consider k1 being Element of NAT  such that
A82: (e / 2) " < k1 by SEQ_4:3;
take i = k1 + m; ::_thesis: ( 1 / (i + 1) < e / 2 & i >= m )
 k1 <= k1 + m by NAT_1:11;
then  (e / 2) " < i by A82, XXREAL_0:2;
then  ((e / 2) ") + 0 < i + 1 by XREAL_1:8;
then  1 / (i + 1) < 1 / ((e / 2) ") by A80, XREAL_1:76;
then  1 / (i + 1) < 1 * (((e / 2) ") ") by XCMPLX_0:def_9;
hence  ( 1 / (i + 1) < e / 2 & i >= m ) by NAT_1:11; ::_thesis: verum
end;
then consider i being Element of NAT  such that
A83: 1 / (i + 1) < e / 2 and
A84: i >= m ;
consider Y0 being finite Subset of X such that
A85: not Y0 is empty and
A86: A . i = Y0 and
A87: seq . i = setsum Y0 by A34;
A88: ||.((setsum Y0) - x).|| < e / 2 by A81, A84, A87;
now__::_thesis:_for_Y1_being_finite_Subset_of_X_st_Y0_c=_Y1_&_Y1_c=_Y_holds_
||.(x_-_(setsum_Y1)).||_<_e
let Y1 be finite Subset of X; ::_thesis: ( Y0 c= Y1 & Y1 c= Y implies ||.(x - (setsum Y1)).|| < e )
assume that
A89: Y0 c= Y1 and
A90: Y1 c= Y ; ::_thesis: ||.(x - (setsum Y1)).|| < e
now__::_thesis:_(_(_Y0_=_Y1_&_||.(x_-_(setsum_Y1)).||_<_e_)_or_(_Y0_<>_Y1_&_||.(x_-_(setsum_Y1)).||_<_e_)_)
percases ( Y0 = Y1 or Y0 <> Y1 ) ;
case Y0 = Y1 ; ::_thesis: ||.(x - (setsum Y1)).|| < e
then ||.(x - (setsum Y1)).|| = ||.(- (x - (setsum Y0))).|| by BHSP_1:31
.= ||.((setsum Y0) - x).|| by RLVECT_1:33 ;
then  ||.(x - (setsum Y1)).|| < e / 2 by A81, A84, A87;
then  ||.(x - (setsum Y1)).|| + 0 < (e / 2) + (e / 2) by A79, XREAL_1:8;
hence  ||.(x - (setsum Y1)).|| < e ; ::_thesis: verum
end;
caseA91: Y0 <> Y1 ; ::_thesis: ||.(x - (setsum Y1)).|| < e
 ex Y2 being finite Subset of X st
( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 )
proof
take Y2 = Y1 \ Y0; ::_thesis: ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 )
A92: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A89, XBOOLE_1:12 ;
hence  ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 ) by A90, A91, A92, XBOOLE_1:1, XBOOLE_1:79; ::_thesis: verum
end;
then consider Y2 being finite Subset of X such that
A93: ( not Y2 is empty & Y2 c= Y ) and
A94: Y0 misses Y2 and
A95: Y0 \/ Y2 = Y1 ;
(setsum Y1) - x = ((setsum Y0) + (setsum Y2)) - x by A1, A94, A95, Th2
.= ((setsum Y0) - x) + (setsum Y2) by RLVECT_1:def_3 ;
then  ||.((setsum Y1) - x).|| <= ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| by BHSP_1:30;
then  ||.(- ((setsum Y1) - x)).|| <= ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| by BHSP_1:31;
then A96: ||.(x + (- (setsum Y1))).|| <= ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| by RLVECT_1:33;
 ||.(setsum Y2).|| < 1 / (i + 1) by A32, A86, A93, A94;
then  ||.(setsum Y2).|| < e / 2 by A83, XXREAL_0:2;
then  ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| < (e / 2) + (e / 2) by A88, XREAL_1:8;
hence  ||.(x - (setsum Y1)).|| < e by A96, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  ||.(x - (setsum Y1)).|| < e ; ::_thesis: verum
end;
hence  ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e ) ) by A85, A86; ::_thesis: verum
end;
hence  Y is summable_set by Def2; ::_thesis: verum
end;
now__::_thesis:_(_Y_is_summable_set_implies_for_e_being_Real_st_e_>_0_holds_
ex_Y0_being_finite_Subset_of_X_st_
(_not_Y0_is_empty_&_Y0_c=_Y_&_(_for_Y1_being_finite_Subset_of_X_st_not_Y1_is_empty_&_Y1_c=_Y_&_Y0_misses_Y1_holds_
||.(setsum_Y1).||_<_e_)_)_)
assume  Y is summable_set ; ::_thesis: for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) )
then consider x being Point of X such that
A97: for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e ) ) by Def2;
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_Y0_being_finite_Subset_of_X_st_
(_not_Y0_is_empty_&_Y0_c=_Y_&_(_for_Y1_being_finite_Subset_of_X_st_not_Y1_is_empty_&_Y1_c=_Y_&_Y0_misses_Y1_holds_
||.(setsum_Y1).||_<_e_)_)
let e be Real; ::_thesis: ( e > 0 implies ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) )
assume  e > 0 ; ::_thesis: ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) )
then consider Y0 being finite Subset of X such that
A98: not Y0 is empty and
A99: Y0 c= Y and
A100: for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e / 2 by A97, XREAL_1:139;
reconsider Y0 = Y0 as non empty finite Subset of X by A98;
now__::_thesis:_for_Y1_being_finite_Subset_of_X_st_not_Y1_is_empty_&_Y1_c=_Y_&_Y0_misses_Y1_holds_
||.(setsum_Y1).||_<_e
let Y1 be finite Subset of X; ::_thesis: ( not Y1 is empty & Y1 c= Y & Y0 misses Y1 implies ||.(setsum Y1).|| < e )
assume that
 not Y1 is empty and
A101: Y1 c= Y and
A102: Y0 misses Y1 ; ::_thesis: ||.(setsum Y1).|| < e
set Z = Y0 \/ Y1;
 Y0 c= Y0 \/ Y1 by XBOOLE_1:7;
then  ||.(x - (setsum (Y0 \/ Y1))).|| < e / 2 by A99, A100, A101, XBOOLE_1:8;
then A103: ||.(x - (setsum (Y0 \/ Y1))).|| + ||.(x - (setsum Y0)).|| < (e / 2) + (e / 2) by A99, A100, XREAL_1:8;
 ||.((x - (setsum (Y0 \/ Y1))) - (x - (setsum Y0))).|| <= ||.(x - (setsum (Y0 \/ Y1))).|| + ||.(- (x - (setsum Y0))).|| by BHSP_1:30;
then A104: ||.((x - (setsum (Y0 \/ Y1))) - (x - (setsum Y0))).|| <= ||.(x - (setsum (Y0 \/ Y1))).|| + ||.(x - (setsum Y0)).|| by BHSP_1:31;
(setsum (Y0 \/ Y1)) - (setsum Y0) = ((setsum Y1) + (setsum Y0)) - (setsum Y0) by A1, A102, Th2
.= (setsum Y1) + ((setsum Y0) + (- (setsum Y0))) by RLVECT_1:def_3
.= (setsum Y1) + (0. X) by RLVECT_1:5
.= setsum Y1 by RLVECT_1:4 ;
then ||.(setsum Y1).|| = ||.(- ((setsum (Y0 \/ Y1)) - (setsum Y0))).|| by BHSP_1:31
.= ||.((setsum Y0) - (setsum (Y0 \/ Y1))).|| by RLVECT_1:33
.= ||.((0. X) + ((setsum Y0) - (setsum (Y0 \/ Y1)))).|| by RLVECT_1:4
.= ||.((x - x) + ((setsum Y0) - (setsum (Y0 \/ Y1)))).|| by RLVECT_1:5
.= ||.(x - (x - ((setsum Y0) - (setsum (Y0 \/ Y1))))).|| by RLVECT_1:29
.= ||.(x - ((x - (setsum Y0)) + (setsum (Y0 \/ Y1)))).|| by RLVECT_1:29
.= ||.((x - (setsum (Y0 \/ Y1))) - (x - (setsum Y0))).|| by RLVECT_1:27 ;
hence  ||.(setsum Y1).|| < e by A104, A103, XXREAL_0:2; ::_thesis: verum
end;
hence  ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) by A99; ::_thesis: verum
end;
hence  for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) ; ::_thesis: verum
end;
hence  ( Y is summable_set iff for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) ) by A2; ::_thesis: verum
end;