let X be RealUnitarySpace; :: thesis:
assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity & X is Hilbert ) ; :: thesis:
let Y be Subset of X; :: thesis:

A2: now

assume Y is summable_set ; :: thesis:
then consider x being Point of X such that
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 Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e ) ) by Def2;

now

let e be Real; :: thesis:
assume A4: e > 0 ; :: thesis:
0 < e / 2 by A4, XREAL_1:141;
then consider Y0 being finite Subset of X such that
A5: ( 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 / 2 ) ) by A3;
reconsider Y0 = Y0 as non empty finite Subset of X by A5;

now

let Y1 be finite Subset of X; :: thesis:
assume A6: ( not Y1 is empty & Y1 c= Y & Y0 misses Y1 ) ; :: thesis:
set Z = Y0 \/ Y1;
(setsum (Y0 \/ Y1)) - (setsum Y0) = ((setsum Y1) + (setsum Y0)) - (setsum Y0) by A1, A6, Th2
.= (setsum Y1) + ((setsum Y0) + (- (setsum Y0))) by RLVECT_1:def 6
.= (setsum Y1) + (0. X) by RLVECT_1:16
.= setsum Y1 by RLVECT_1:10 ;
then A7: ||.(setsum Y1).|| = ||.(- ((setsum (Y0 \/ Y1)) - (setsum Y0))).|| by BHSP_1:37
.= ||.((setsum Y0) - (setsum (Y0 \/ Y1))).|| by RLVECT_1:47
.= ||.((0. X) + ((setsum Y0) - (setsum (Y0 \/ Y1)))).|| by RLVECT_1:10
.= ||.((x - x) + ((setsum Y0) - (setsum (Y0 \/ Y1)))).|| by RLVECT_1:16
.= ||.(x - (x - ((setsum Y0) - (setsum (Y0 \/ Y1))))).|| by RLVECT_1:43
.= ||.(x - ((x - (setsum Y0)) + (setsum (Y0 \/ Y1)))).|| by RLVECT_1:43
.= ||.((x - (setsum (Y0 \/ Y1))) - (x - (setsum Y0))).|| by RLVECT_1:41 ;
||.((x - (setsum (Y0 \/ Y1))) - (x - (setsum Y0))).|| <= ||.(x - (setsum (Y0 \/ Y1))).|| + ||.(- (x - (setsum Y0))).|| by BHSP_1:36;
then A8: ||.((x - (setsum (Y0 \/ Y1))) - (x - (setsum Y0))).|| <= ||.(x - (setsum (Y0 \/ Y1))).|| + ||.(x - (setsum Y0)).|| by BHSP_1:37;
( Y0 c= Y0 \/ Y1 & Y0 \/ Y1 c= Y ) by A5, A6, XBOOLE_1:7, XBOOLE_1:8;
then ||.(x - (setsum (Y0 \/ Y1))).|| < e / 2 by A5;
then ||.(x - (setsum (Y0 \/ Y1))).|| + ||.(x - (setsum Y0)).|| < (e / 2) + (e / 2) by A5, XREAL_1:10;
hence ||.(setsum Y1).|| < e by A7, A8, XXREAL_0:2; :: thesis:

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 A5; :: thesis:

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:

end;

now

assume A9: 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:
defpred S₁[ 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) ) );
A10: ex B being Function of NAT ,(bool Y) st
for x being set st x in NAT holds
S₁[x,B . x]

proof

A11: now

let x be set ; :: thesis:
assume A12: x in NAT ; :: thesis:
reconsider xx = x as Element of NAT by A12;
reconsider e = 1 / (xx + 1) as Real ;
0 / (xx + 1) < 1 / (xx + 1) by XREAL_1:76;
then consider Y0 being finite Subset of X such that
A13: ( 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 A9;
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 A13;
hence ex y being set st
( y in bool Y & S₁[x,y] ) by A13; :: thesis:

end;

thus ex B being Function of NAT ,(bool Y) st
for x being set st x in NAT holds
S₁[x,B . x] from FUNCT_2:sch 1(A11); :: thesis:

end;

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
A14: 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 A10;
deffunc H₁( 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) = H₁(n,A . n) ) ) from NAT_1:sch 11();
then consider A being Function such that
A15: ( dom A = NAT & A . 0 = B . 0 & ( for n being Nat holds A . (n + 1) = (B . (n + 1)) \/ (A . n) ) ) ;
defpred S₂[ 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 ) );
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:
assume A16: j0 = 0 ; :: thesis:
defpred S₃[ Element of NAT ] means ( j0 <= $1 implies A . j0 c= A . $1 );
A17: S₃[ 0 ] ;

A18: now

let j be Element of NAT ; :: thesis:
assume A19: S₃[j] ; :: thesis:
A . (j + 1) = (B . (j + 1)) \/ (A . j) by A15;
then A . j c= A . (j + 1) by XBOOLE_1:7;
hence S₃[j + 1] by A16, A19, XBOOLE_1:1; :: thesis:

end;

thus for j being Element of NAT holds S₃[j] from NAT_1:sch 1(A17, A18); :: thesis:

end;

then A20: S₂[ 0 ] by A14, A15;

A21: now

let n be Element of NAT ; :: thesis:
assume A22: S₂[n] ; :: thesis:
A23: A . (n + 1) = (B . (n + 1)) \/ (A . n) by A15;
A24: B . (n + 1) is finite Subset of X by A14;
A26: 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:
assume A27: ( not Y1 is empty & Y1 c= Y & A . (n + 1) misses Y1 ) ; :: thesis:
A . (n + 1) = (B . (n + 1)) \/ (A . n) by A15;
then B . (n + 1) misses Y1 by A27, XBOOLE_1:7, XBOOLE_1:63;
hence ||.(setsum Y1).|| < 1 / ((n + 1) + 1) by A14, A27; :: thesis:

end;

defpred S₃[ Element of NAT ] means ( n + 1 <= $1 implies A . (n + 1) c= A . $1 );
for j being Element of NAT holds S₃[j]

proof

A28: S₃[ 0 ] ;
A29: for j being Element of NAT st S₃[j] holds
S₃[j + 1]

proof

let j be Element of NAT ; :: thesis:
assume that
A30: ( n + 1 <= j implies A . (n + 1) c= A . j ) and
A31: n + 1 <= j + 1 ; :: thesis:

per cases ;

suppose n = j ; :: thesis:

hence A . (n + 1) c= A . (j + 1) ; :: thesis:

end;

suppose A32: n <> j ; :: thesis:

n <= j by A31, XREAL_1:8;
then A33: n < j by A32, XXREAL_0:1;
A . (j + 1) = (B . (j + 1)) \/ (A . j) by A15;
then A . j c= A . (j + 1) by XBOOLE_1:7;
hence A . (n + 1) c= A . (j + 1) by A30, A33, NAT_1:13, XBOOLE_1:1; :: thesis:

end;

thus for j being Element of NAT holds S₃[j] from NAT_1:sch 1(A28, A29); :: thesis:

end;

hence S₂[n + 1] by A22, A23, A24, A26, XBOOLE_1:8; :: thesis:

end;

A34: for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A20, A21);

now

let y be set ; :: thesis:
assume A35: y in rng A ; :: thesis:
consider x being set such that
A36: ( x in dom A & y = A . x ) by A35, FUNCT_1:def 5;
reconsider i = x as Element of NAT by A15, A36;
A . i c= Y by A34;
hence y in bool Y by A36; :: thesis:

end;

then rng A c= bool Y by TARSKI:def 3;
then A is Function of NAT ,(bool Y) by A15, FUNCT_2:4;
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 A34; :: thesis:

end;

then consider A being Function of NAT ,(bool Y) such that
A37: 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 S₂[ set , set ] means ex Y1 being finite Subset of X st
( not Y1 is empty & A . $1 = Y1 & $2 = setsum Y1 );
A38: for x being set st x in NAT holds
ex y being set st
( y in the carrier of X & S₂[x,y] )

proof

let x be set ; :: thesis:
assume A39: x in NAT ; :: thesis:
reconsider i = x as Element of NAT by A39;
A40: ( 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 . x misses Y1 holds
||.(setsum Y1).|| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds
A . i c= A . j ) ) by A37;
then reconsider Y1 = A . x as finite Subset of X ;
reconsider y = setsum Y1 as set ;
( y in the carrier of X & ex Y1 being finite Subset of X st
( Y1 is non empty set & A . x = Y1 & y = setsum Y1 ) ) by A40;
hence ex y being set st
( y in the carrier of X & S₂[x,y] ) ; :: thesis:

end;

ex F being Function of NAT ,the carrier of X st
for x being set st x in NAT holds
S₂[x,F . x] from FUNCT_2:sch 1(A38);
then consider F being Function of NAT ,the carrier of X such that
A41: 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 ;
A42: seq is Cauchy

proof

now

let e be Real; :: thesis:
assume A43: e > 0 ; :: thesis:
A44: e / 2 > 0 / 2 by A43, XREAL_1:76;
ex k being Element of NAT st 1 / (k + 1) < e / 2

proof

set p = e / 2;
A45: 0 < (e / 2) " by A44;
consider k1 being Element of NAT such that
A46: (e / 2) " < k1 by SEQ_4:10;
take k = k1; :: thesis:
((e / 2) " ) + 0 < k1 + 1 by A46, XREAL_1:10;
then 1 / (k1 + 1) < 1 / ((e / 2) " ) by A45, XREAL_1:78;
then 1 / (k + 1) < 1 * (((e / 2) " ) " ) by XCMPLX_0:def 9;
hence 1 / (k + 1) < e / 2 ; :: thesis:

end;

then consider k being Element of NAT such that
A47: 1 / (k + 1) < e / 2 ;

now

let n, m be Element of NAT ; :: thesis:
assume A48: ( n >= k & m >= k ) ; :: thesis:
consider Y0 being finite Subset of X such that
A49: ( not Y0 is empty & A . k = Y0 & seq . k = setsum Y0 ) by A41;
consider Y1 being finite Subset of X such that
A50: ( not Y1 is empty & A . n = Y1 & seq . n = setsum Y1 ) by A41;
consider Y2 being finite Subset of X such that
A51: ( not Y2 is empty & A . m = Y2 & seq . m = setsum Y2 ) by A41;
A52: Y0 c= Y1 by A37, A48, A49, A50;
A53: Y0 c= Y2 by A37, A48, A49, A51;

now

per cases ;

case A54: Y0 = Y1 ; :: thesis:

now

per cases ;

case Y0 = Y2 ; :: thesis:

then (seq . n) - (seq . m) = 0. X by A50, A51, A54, RLVECT_1:16;
hence ||.((seq . n) - (seq . m)).|| < e by A43, BHSP_1:32; :: thesis:

end;

case A55: Y0 <> Y2 ; :: thesis:

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:
A56: Y2 \ Y0 c= Y2 by XBOOLE_1:36;
Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
.= Y2 by A53, XBOOLE_1:12 ;
hence ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A51, A55, A56, XBOOLE_1:1, XBOOLE_1:79; :: thesis:

end;

then consider Y02 being finite Subset of X such that
A57: ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) ;
A58: setsum Y2 = (setsum Y0) + (setsum Y02) by A1, A57, Th2;
||.(setsum Y02).|| < 1 / (k + 1) by A37, A49, A57;
then A59: ||.(setsum Y02).|| < e / 2 by A47, XXREAL_0:2;
A60: e * (1 / 2) < e * 1 by A43, XREAL_1:70;
||.((seq . n) - (seq . m)).|| = ||.(((setsum Y0) - (setsum Y0)) - (setsum Y02)).|| by A50, A51, A54, A58, RLVECT_1:41
.= ||.((0. X) - (setsum Y02)).|| by RLVECT_1:28
.= ||.(- (setsum Y02)).|| by RLVECT_1:27
.= ||.(setsum Y02).|| by BHSP_1:37 ;
hence ||.((seq . n) - (seq . m)).|| < e by A59, A60, XXREAL_0:2; :: thesis:

end;

hence ||.((seq . n) - (seq . m)).|| < e ; :: thesis:

end;

case A61: Y0 <> Y1 ; :: thesis:

now

per cases ;

case A62: Y0 = Y2 ; :: thesis:

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:
A63: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A52, XBOOLE_1:12 ;
hence ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A50, A61, A63, XBOOLE_1:1, XBOOLE_1:79; :: thesis:

end;

then consider Y01 being finite Subset of X such that
A64: ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) ;
seq . n = (seq . k) + (setsum Y01) by A1, A49, A50, A64, Th2;
then A65: (seq . n) - (seq . k) = (seq . k) + ((setsum Y01) + (- (seq . k))) by RLVECT_1:def 6
.= (seq . k) - ((seq . k) - (setsum Y01)) by RLVECT_1:47
.= ((setsum Y0) - (setsum Y0)) + (setsum Y01) by A49, RLVECT_1:43
.= (0. X) + (setsum Y01) by RLVECT_1:16
.= setsum Y01 by RLVECT_1:10 ;
A66: (seq . k) - (seq . m) = 0. X by A49, A51, A62, RLVECT_1:16;
(seq . n) - (seq . m) = ((seq . n) - (seq . m)) + (0. X) by RLVECT_1:10
.= ((seq . n) - (seq . m)) + ((seq . k) - (seq . k)) by RLVECT_1:16
.= (seq . n) - ((seq . m) - ((seq . k) - (seq . k))) by RLVECT_1:43
.= (seq . n) - (((seq . m) - (seq . k)) + (seq . k)) by RLVECT_1:43
.= (seq . n) - ((seq . k) - ((seq . k) - (seq . m))) by RLVECT_1:47
.= (setsum Y01) + (0. X) by A65, A66, RLVECT_1:43 ;
then ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(0. X).|| by BHSP_1:36;
then A67: ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + 0 by BHSP_1:32;
||.(setsum Y01).|| < 1 / (k + 1) by A37, A49, A64;
then ||.(setsum Y01).|| < e / 2 by A47, XXREAL_0:2;
then ||.((seq . n) - (seq . m)).|| < e / 2 by A67, XXREAL_0:2;
then ||.((seq . n) - (seq . m)).|| + 0 < (e / 2) + (e / 2) by A43, XREAL_1:10;
hence ||.((seq . n) - (seq . m)).|| < e ; :: thesis:

end;

case A68: Y0 <> Y2 ; :: thesis:

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:
A69: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A52, XBOOLE_1:12 ;
hence ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A50, A61, A69, XBOOLE_1:1, XBOOLE_1:79; :: thesis:

end;

then consider Y01 being finite Subset of X such that
A70: ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) ;
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:
A71: Y2 \ Y0 c= Y2 by XBOOLE_1:36;
Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
.= Y2 by A53, XBOOLE_1:12 ;
hence ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A51, A68, A71, XBOOLE_1:1, XBOOLE_1:79; :: thesis:

end;

then consider Y02 being finite Subset of X such that
A72: ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) ;
||.(setsum Y01).|| < 1 / (k + 1) by A37, A49, A70;
then A73: ||.(setsum Y01).|| < e / 2 by A47, XXREAL_0:2;
||.(setsum Y02).|| < 1 / (k + 1) by A37, A49, A72;
then ||.(setsum Y02).|| < e / 2 by A47, XXREAL_0:2;
then A74: ||.(setsum Y01).|| + ||.(setsum Y02).|| < (e / 2) + (e / 2) by A73, XREAL_1:10;
A75: setsum Y1 = (setsum Y0) + (setsum Y01) by A1, A70, Th2;
A76: setsum Y2 = (setsum Y0) + (setsum Y02) by A1, A72, Th2;
A77: (seq . n) - (seq . k) = (setsum Y01) + ((seq . k) + (- (seq . k))) by A49, A50, A75, RLVECT_1:def 6
.= (setsum Y01) + (0. X) by RLVECT_1:16
.= setsum Y01 by RLVECT_1:10 ;
A78: (seq . m) - (seq . k) = (setsum Y02) + ((seq . k) + (- (seq . k))) by A49, A51, A76, RLVECT_1:def 6
.= (setsum Y02) + (0. X) by RLVECT_1:16
.= setsum Y02 by RLVECT_1:10 ;
(seq . n) - (seq . m) = ((seq . n) - (seq . m)) + (0. X) by RLVECT_1:10
.= ((seq . n) - (seq . m)) + ((seq . k) - (seq . k)) by RLVECT_1:16
.= (seq . n) - ((seq . m) - ((seq . k) - (seq . k))) by RLVECT_1:43
.= (seq . n) - (((seq . m) - (seq . k)) + (seq . k)) by RLVECT_1:43
.= (seq . n) - ((seq . k) - ((seq . k) - (seq . m))) by RLVECT_1:47
.= ((seq . n) - (seq . k)) + ((seq . k) + (- (seq . m))) by RLVECT_1:43
.= (setsum Y01) + (- (setsum Y02)) by A77, A78, RLVECT_1:47 ;
then ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(- (setsum Y02)).|| by BHSP_1:36;
then ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(setsum Y02).|| by BHSP_1:37;
hence ||.((seq . n) - (seq . m)).|| < e by A74, XXREAL_0:2; :: thesis:

end;

hence ||.((seq . n) - (seq . m)).|| < e ; :: thesis:

end;

hence ||.((seq . n) - (seq . m)).|| < e ; :: thesis:

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:

end;

hence seq is Cauchy by BHSP_3:2; :: thesis:

end;

X is complete by A1, BHSP_3:def 7;
then seq is convergent by A42, BHSP_3:def 6;
then consider x being Point of X such that
A79: 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

let e be Real; :: thesis:
assume A80: e > 0 ; :: thesis:
A81: e / 2 > 0 / 2 by A80, XREAL_1:76;
then consider m being Element of NAT such that
A82: for n being Element of NAT st n >= m holds
||.((seq . n) - x).|| < e / 2 by A79;
ex i being Element of NAT st
( 1 / (i + 1) < e / 2 & i >= m )

proof

set p = e / 2;
A83: 0 < (e / 2) " by A81;
consider k1 being Element of NAT such that
A84: (e / 2) " < k1 by SEQ_4:10;
take i = k1 + m; :: thesis:
k1 <= k1 + m by NAT_1:11;
then (e / 2) " < i by A84, XXREAL_0:2;
then ((e / 2) " ) + 0 < i + 1 by XREAL_1:10;
then 1 / (i + 1) < 1 / ((e / 2) " ) by A83, XREAL_1:78;
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:

end;

then consider i being Element of NAT such that
A85: ( 1 / (i + 1) < e / 2 & i >= m ) ;
consider Y0 being finite Subset of X such that
A86: ( not Y0 is empty & A . i = Y0 & seq . i = setsum Y0 ) by A41;
A87: ||.((setsum Y0) - x).|| < e / 2 by A82, A85, A86;

now

let Y1 be finite Subset of X; :: thesis:
assume A88: ( Y0 c= Y1 & Y1 c= Y ) ; :: thesis:

now

per cases ;

case Y0 = Y1 ; :: thesis:

then ||.(x - (setsum Y1)).|| = ||.(- (x - (setsum Y0))).|| by BHSP_1:37
.= ||.((setsum Y0) - x).|| by RLVECT_1:47 ;
then ||.(x - (setsum Y1)).|| < e / 2 by A82, A85, A86;
then ||.(x - (setsum Y1)).|| + 0 < (e / 2) + (e / 2) by A80, XREAL_1:10;
hence ||.(x - (setsum Y1)).|| < e ; :: thesis:

end;

case A89: Y0 <> Y1 ; :: thesis:

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:
A90: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A88, XBOOLE_1:12 ;
hence ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 ) by A88, A89, A90, XBOOLE_1:1, XBOOLE_1:79; :: thesis:

end;

then consider Y2 being finite Subset of X such that
A91: ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 ) ;
||.(setsum Y2).|| < 1 / (i + 1) by A37, A86, A91;
then A92: ||.(setsum Y2).|| < e / 2 by A85, XXREAL_0:2;
(setsum Y1) - x = ((setsum Y0) + (setsum Y2)) - x by A1, A91, Th2
.= ((setsum Y0) - x) + (setsum Y2) by RLVECT_1:def 6 ;
then ||.((setsum Y1) - x).|| <= ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| by BHSP_1:36;
then ||.(- ((setsum Y1) - x)).|| <= ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| by BHSP_1:37;
then A93: ||.(x + (- (setsum Y1))).|| <= ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| by RLVECT_1:47;
||.((setsum Y0) - x).|| + ||.(setsum Y2).|| < (e / 2) + (e / 2) by A87, A92, XREAL_1:10;
hence ||.(x - (setsum Y1)).|| < e by A93, XXREAL_0:2; :: thesis:

end;

hence ||.(x - (setsum Y1)).|| < e ; :: thesis:

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 A86; :: thesis:

end;

hence Y is summable_set by Def2; :: thesis:

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: