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 ) ) )

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

( 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 )

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 S_{1}[ object , object ] means ex D2 being set st

( D2 = $2 & $2 is finite Subset of X & not D2 is empty & D2 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 & D2 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: for x being object st x in NAT holds

ex y being object st

( y in bool Y & S_{1}[x,y] )

A7: for x being object st x in NAT holds

S_{1}[x,B . x]
from FUNCT_2:sch 1(A4);

ex A being sequence of (bool Y) st

for i being 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 Nat st i <= j holds

A . i c= A . j ) )

A33: for i being 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 Nat st i <= j holds

A . i c= A . j ) ) ;

defpred S_{2}[ object , object ] means ex Y1 being finite Subset of X st

( not Y1 is empty & A . $1 = Y1 & $2 = setsum Y1 );

A34: for x being object st x in NAT holds

ex y being object st

( y in the carrier of X & S_{2}[x,y] )

for x being object st x in NAT holds

S_{2}[x,F . x]
from FUNCT_2:sch 1(A34);

then consider F being sequence of the carrier of X such that

A35: for x being object 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 ;

then seq is convergent by BHSP_3:def 4;

then consider x being Point of X such that

A80: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq . n) - x).|| < r by BHSP_2:9;

end;( D2 = $2 & $2 is finite Subset of X & not D2 is empty & D2 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 & D2 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: for x being object st x in NAT holds

ex y being object st

( y in bool Y & S

proof

consider B being sequence of (bool Y) such that
let x be object ; :: thesis: ( x in NAT implies ex y being object st

( y in bool Y & S_{1}[x,y] ) )

assume x in NAT ; :: thesis: ex y being object st

( y in bool Y & S_{1}[x,y] )

then reconsider xx = x as Nat ;

reconsider e = 1 / (xx + 1) as Real ;

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;

reconsider Y0 = Y0 as object ;

take Y0 ; :: thesis: ( Y0 in bool Y & S_{1}[x,Y0] )

thus Y0 in bool Y by A5; :: thesis: S_{1}[x,Y0]

take Y0 ; :: thesis: ( Y0 is set & Y0 = Y0 & Y0 is finite Subset of X & not Y0 is empty & Y0 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 & Y0 misses Y1 holds

||.(setsum Y1).|| < 1 / (z + 1) ) )

thus ( Y0 is set & Y0 = Y0 & Y0 is finite Subset of X & not Y0 is empty & Y0 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 & Y0 misses Y1 holds

||.(setsum Y1).|| < 1 / (z + 1) ) ) by A5, A6; :: thesis: verum

end;( y in bool Y & S

assume x in NAT ; :: thesis: ex y being object st

( y in bool Y & S

then reconsider xx = x as Nat ;

reconsider e = 1 / (xx + 1) as Real ;

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;

reconsider Y0 = Y0 as object ;

take Y0 ; :: thesis: ( Y0 in bool Y & S

thus Y0 in bool Y by A5; :: thesis: S

take Y0 ; :: thesis: ( Y0 is set & Y0 = Y0 & Y0 is finite Subset of X & not Y0 is empty & Y0 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 & Y0 misses Y1 holds

||.(setsum Y1).|| < 1 / (z + 1) ) )

thus ( Y0 is set & Y0 = Y0 & Y0 is finite Subset of X & not Y0 is empty & Y0 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 & Y0 misses Y1 holds

||.(setsum Y1).|| < 1 / (z + 1) ) ) by A5, A6; :: thesis: verum

A7: for x being object st x in NAT holds

S

ex A being sequence of (bool Y) st

for i being 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 Nat st i <= j holds

A . i c= A . j ) )

proof

then consider A being sequence of (bool Y) such that
A8:
for x being object 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) ) )_{1}( 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_{1}(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 S_{2}[ 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 Nat st $1 <= j holds

A . $1 c= A . j ) );

for j being Nat st j0 <= j holds

A . j0 c= A . j_{2}[ 0 ]
by A8, A10;

A30: for i being Nat holds S_{2}[i]
from NAT_1:sch 2(A29, A12);

then A is sequence of (bool Y) by A9, FUNCT_2:2;

hence ex A being sequence of (bool Y) st

for i being 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 Nat st i <= j holds

A . i c= A . j ) ) by A30; :: thesis: verum

end;( 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) ) )

proof

deffunc H
let x be object ; :: thesis: ( x in NAT implies ( 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) ) ) )

assume x in NAT ; :: thesis: ( 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) ) )

then S_{1}[x,B . x]
by A7;

hence ( 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) ) ) ; :: thesis: verum

end;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) ) ) )

assume x in NAT ; :: thesis: ( 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) ) )

then S

hence ( 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) ) ) ; :: thesis: verum

ex A being Function st

( dom A = NAT & A . 0 = B . 0 & ( for n being Nat holds A . (n + 1) = H

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 S

||.(setsum Y1).|| < 1 / ($1 + 1) ) & ( for j being Nat st $1 <= j holds

A . $1 c= A . j ) );

A12: now :: thesis: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]

for j0 being Nat st j0 = 0 holds S

let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume A13: S_{2}[n]
; :: thesis: S_{2}[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)_{3}[ Nat] means ( n + 1 <= $1 implies A . (n + 1) c= A . $1 );

A17: for j being Nat st S_{3}[j] holds

S_{3}[j + 1]
_{3}[ 0 ]
;

A23: for j being Nat holds S_{3}[j]
from NAT_1:sch 2(A22, A17);

A24: ( A . (n + 1) = (B . (n + 1)) \/ (A . n) & B . (n + 1) is finite Subset of X ) by A8, A11;

thus S_{2}[n + 1]
by A13, A14, A23, XBOOLE_1:8, A24; :: thesis: verum

end;assume A13: S

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

defpred S
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;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

A17: for j being Nat st S

S

proof

A22:
S
let j be Nat; :: thesis: ( S_{3}[j] implies S_{3}[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)

end;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)

A23: for j being Nat holds S

A24: ( A . (n + 1) = (B . (n + 1)) \/ (A . n) & B . (n + 1) is finite Subset of X ) by A8, A11;

thus S

for j being Nat st j0 <= j holds

A . j0 c= A . j

proof

then A29:
S
let j0 be Nat; :: thesis: ( j0 = 0 implies for j being Nat st j0 <= j holds

A . j0 c= A . j )

assume A25: j0 = 0 ; :: thesis: for j being Nat st j0 <= j holds

A . j0 c= A . j

defpred S_{3}[ Nat] means ( j0 <= $1 implies A . j0 c= A . $1 );

_{3}[ 0 ]
;

thus for j being Nat holds S_{3}[j]
from NAT_1:sch 2(A28, A26); :: thesis: verum

end;A . j0 c= A . j )

assume A25: j0 = 0 ; :: thesis: for j being Nat st j0 <= j holds

A . j0 c= A . j

defpred S

A26: now :: thesis: for j being Nat st S_{3}[j] holds

S_{3}[j + 1]

A28:
SS

let j be Nat; :: thesis: ( S_{3}[j] implies S_{3}[j + 1] )

assume A27: S_{3}[j]
; :: thesis: S_{3}[j + 1]

A . (j + 1) = (B . (j + 1)) \/ (A . j) by A11;

then A . j c= A . (j + 1) by XBOOLE_1:7;

hence S_{3}[j + 1]
by A25, A27, XBOOLE_1:1; :: thesis: verum

end;assume A27: S

A . (j + 1) = (B . (j + 1)) \/ (A . j) by A11;

then A . j c= A . (j + 1) by XBOOLE_1:7;

hence S

thus for j being Nat holds S

A30: for i being Nat holds S

now :: thesis: for y being object st y in rng A holds

y in bool Y

then
rng A c= bool Y
by TARSKI:def 3;y in bool Y

let y be object ; :: thesis: ( y in rng A implies y in bool Y )

assume y in rng A ; :: thesis: y in bool Y

then consider x being object such that

A31: x in dom A and

A32: y = A . x by FUNCT_1:def 3;

reconsider i = x as Nat by A9, A31;

A . i c= Y by A30;

hence y in bool Y by A32; :: thesis: verum

end;assume y in rng A ; :: thesis: y in bool Y

then consider x being object such that

A31: x in dom A and

A32: y = A . x by FUNCT_1:def 3;

reconsider i = x as Nat by A9, A31;

A . i c= Y by A30;

hence y in bool Y by A32; :: thesis: verum

then A is sequence of (bool Y) by A9, FUNCT_2:2;

hence ex A being sequence of (bool Y) st

for i being 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 Nat st i <= j holds

A . i c= A . j ) ) by A30; :: thesis: verum

A33: for i being 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 Nat st i <= j holds

A . i c= A . j ) ) ;

defpred S

( not Y1 is empty & A . $1 = Y1 & $2 = setsum Y1 );

A34: for x being object st x in NAT holds

ex y being object st

( y in the carrier of X & S

proof

ex F being sequence of the carrier of X st
let x be object ; :: thesis: ( x in NAT implies ex y being object st

( y in the carrier of X & S_{2}[x,y] ) )

assume x in NAT ; :: thesis: ex y being object st

( y in the carrier of X & S_{2}[x,y] )

then reconsider i = x as Nat ;

A . i is finite Subset of X by A33;

then reconsider Y1 = A . x as finite Subset of X ;

reconsider y = setsum Y1 as set ;

not A . i is empty by A33;

then ex Y1 being finite Subset of X st

( Y1 is non empty set & A . x = Y1 & y = setsum Y1 ) ;

hence ex y being object st

( y in the carrier of X & S_{2}[x,y] )
; :: thesis: verum

end;( y in the carrier of X & S

assume x in NAT ; :: thesis: ex y being object st

( y in the carrier of X & S

then reconsider i = x as Nat ;

A . i is finite Subset of X by A33;

then reconsider Y1 = A . x as finite Subset of X ;

reconsider y = setsum Y1 as set ;

not A . i is empty by A33;

then ex Y1 being finite Subset of X st

( Y1 is non empty set & A . x = Y1 & y = setsum Y1 ) ;

hence ex y being object st

( y in the carrier of X & S

for x being object st x in NAT holds

S

then consider F being sequence of the carrier of X such that

A35: for x being object 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 Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < e

then
seq is Cauchy
by BHSP_3:2;ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < e

let e be Real; :: thesis: ( e > 0 implies ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < e )

assume A36: e > 0 ; :: thesis: ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < e

A37: e / 2 > 0 / 2 by A36, XREAL_1:74;

ex k being Nat st 1 / (k + 1) < e / 2

A39: 1 / (k + 1) < e / 2 ;

for n, m being Nat st n >= k & m >= k holds

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

end;for n, m being Nat st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < e )

assume A36: e > 0 ; :: thesis: ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < e

A37: e / 2 > 0 / 2 by A36, XREAL_1:74;

ex k being Nat st 1 / (k + 1) < e / 2

proof

then consider k being Nat such that
set p = e / 2;

consider k1 being Nat such that

A38: (e / 2) " < k1 by SEQ_4:3;

take k = k1; :: thesis: 1 / (k + 1) < e / 2

((e / 2) ") + 0 < k1 + 1 by A38, XREAL_1:8;

then 1 / (k1 + 1) < 1 / ((e / 2) ") by A37, XREAL_1:76;

then 1 / (k + 1) < 1 * (((e / 2) ") ") by XCMPLX_0:def 9;

hence 1 / (k + 1) < e / 2 ; :: thesis: verum

end;consider k1 being Nat such that

A38: (e / 2) " < k1 by SEQ_4:3;

take k = k1; :: thesis: 1 / (k + 1) < e / 2

((e / 2) ") + 0 < k1 + 1 by A38, XREAL_1:8;

then 1 / (k1 + 1) < 1 / ((e / 2) ") by A37, XREAL_1:76;

then 1 / (k + 1) < 1 * (((e / 2) ") ") by XCMPLX_0:def 9;

hence 1 / (k + 1) < e / 2 ; :: thesis: verum

A39: 1 / (k + 1) < e / 2 ;

now :: thesis: for nn, mm being Nat st nn >= k & mm >= k holds

||.((seq . nn) - (seq . mm)).|| < e

hence
ex k being Nat st ||.((seq . nn) - (seq . mm)).|| < e

let nn, mm be Nat; :: thesis: ( nn >= k & mm >= k implies ||.((seq . nn) - (seq . mm)).|| < e )

assume that

A40: nn >= k and

A41: mm >= k ; :: thesis: ||.((seq . nn) - (seq . mm)).|| < e

( nn in NAT & mm in NAT & k in NAT ) by ORDINAL1:def 12;

then reconsider k = k, m = mm, n = nn as Element of NAT ;

consider Y2 being finite Subset of X such that

not Y2 is empty and

A42: A . m = Y2 and

A43: seq . m = setsum Y2 by A35;

consider Y0 being finite Subset of X such that

not Y0 is empty and

A44: A . k = Y0 and

A45: seq . k = setsum Y0 by A35;

A46: Y0 c= Y2 by A33, A41, A44, A42;

consider Y1 being finite Subset of X such that

not Y1 is empty and

A47: A . n = Y1 and

A48: seq . n = setsum Y1 by A35;

A49: Y0 c= Y1 by A33, A40, A44, A47;

end;assume that

A40: nn >= k and

A41: mm >= k ; :: thesis: ||.((seq . nn) - (seq . mm)).|| < e

( nn in NAT & mm in NAT & k in NAT ) by ORDINAL1:def 12;

then reconsider k = k, m = mm, n = nn as Element of NAT ;

consider Y2 being finite Subset of X such that

not Y2 is empty and

A42: A . m = Y2 and

A43: seq . m = setsum Y2 by A35;

consider Y0 being finite Subset of X such that

not Y0 is empty and

A44: A . k = Y0 and

A45: seq . k = setsum Y0 by A35;

A46: Y0 c= Y2 by A33, A41, A44, A42;

consider Y1 being finite Subset of X such that

not Y1 is empty and

A47: A . n = Y1 and

A48: seq . n = setsum Y1 by A35;

A49: Y0 c= Y1 by A33, A40, A44, A47;

now :: thesis: ( ( Y0 = Y1 & ||.((seq . n) - (seq . m)).|| < e ) or ( Y0 <> Y1 & ||.((seq . n) - (seq . m)).|| < e ) )end;

hence
||.((seq . nn) - (seq . mm)).|| < e
; :: thesis: verumper cases
( Y0 = Y1 or Y0 <> Y1 )
;

end;

case A50:
Y0 = Y1
; :: thesis: ||.((seq . n) - (seq . m)).|| < e

end;

now :: thesis: ( ( Y0 = Y2 & ||.((seq . n) - (seq . m)).|| < e ) or ( Y0 <> Y2 & ||.((seq . n) - (seq . m)).|| < e ) )end;

hence
||.((seq . n) - (seq . m)).|| < e
; :: thesis: verumper cases
( Y0 = Y2 or Y0 <> Y2 )
;

end;

case
Y0 = Y2
; :: thesis: ||.((seq . n) - (seq . m)).|| < e

then
(seq . n) - (seq . m) = 0. X
by A48, A43, A50, RLVECT_1:5;

hence ||.((seq . n) - (seq . m)).|| < e by A36, BHSP_1:26; :: thesis: verum

end;hence ||.((seq . n) - (seq . m)).|| < e by A36, BHSP_1:26; :: thesis: verum

case A51:
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 )

A54: ( not Y02 is empty & Y02 c= Y ) and

A55: Y02 misses Y0 and

A56: Y0 \/ Y02 = Y2 ;

||.(setsum Y02).|| < 1 / (k + 1) by A33, A44, A54, A55;

then A57: ||.(setsum Y02).|| < e / 2 by A39, XXREAL_0:2;

setsum Y2 = (setsum Y0) + (setsum Y02) by A1, A55, A56, Th2;

then A58: ||.((seq . n) - (seq . m)).|| = ||.(((setsum Y0) - (setsum Y0)) - (setsum Y02)).|| by A48, A43, A50, 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 A36, XREAL_1:68;

hence ||.((seq . n) - (seq . m)).|| < e by A57, A58, XXREAL_0:2; :: thesis: verum

end;( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )

proof

then consider Y02 being finite Subset of X such that
take Y02 = Y2 \ Y0; :: thesis: ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )

A52: Y2 \ Y0 c= Y2 by XBOOLE_1:36;

A53: Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39

.= Y2 by A46, XBOOLE_1:12 ;

hence not Y02 is empty by A51; :: thesis: ( Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )

thus Y02 c= Y by A42, A52, XBOOLE_1:1; :: thesis: ( Y02 misses Y0 & Y0 \/ Y02 = Y2 )

thus ( Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by XBOOLE_1:79, A53; :: thesis: verum

end;A52: Y2 \ Y0 c= Y2 by XBOOLE_1:36;

A53: Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39

.= Y2 by A46, XBOOLE_1:12 ;

hence not Y02 is empty by A51; :: thesis: ( Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )

thus Y02 c= Y by A42, A52, XBOOLE_1:1; :: thesis: ( Y02 misses Y0 & Y0 \/ Y02 = Y2 )

thus ( Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by XBOOLE_1:79, A53; :: thesis: verum

A54: ( not Y02 is empty & Y02 c= Y ) and

A55: Y02 misses Y0 and

A56: Y0 \/ Y02 = Y2 ;

||.(setsum Y02).|| < 1 / (k + 1) by A33, A44, A54, A55;

then A57: ||.(setsum Y02).|| < e / 2 by A39, XXREAL_0:2;

setsum Y2 = (setsum Y0) + (setsum Y02) by A1, A55, A56, Th2;

then A58: ||.((seq . n) - (seq . m)).|| = ||.(((setsum Y0) - (setsum Y0)) - (setsum Y02)).|| by A48, A43, A50, 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 A36, XREAL_1:68;

hence ||.((seq . n) - (seq . m)).|| < e by A57, A58, XXREAL_0:2; :: thesis: verum

case A59:
Y0 <> Y1
; :: thesis: ||.((seq . n) - (seq . m)).|| < e

end;

now :: thesis: ( ( Y0 = Y2 & ||.((seq . n) - (seq . m)).|| < e ) or ( Y0 <> Y2 & ||.((seq . n) - (seq . m)).|| < e ) )end;

hence
||.((seq . n) - (seq . m)).|| < e
; :: thesis: verumper cases
( Y0 = Y2 or Y0 <> Y2 )
;

end;

case
Y0 = Y2
; :: thesis: ||.((seq . n) - (seq . m)).|| < e

then A60:
(seq . k) - (seq . m) = 0. X
by A45, A43, RLVECT_1:5;

ex Y01 being finite Subset of X st

( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )

A62: ( not Y01 is empty & Y01 c= Y ) and

A63: Y01 misses Y0 and

A64: Y0 \/ Y01 = Y1 ;

seq . n = (seq . k) + (setsum Y01) by A1, A45, A48, A63, A64, Th2;

then A65: (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 A45, 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 A65, A60, RLVECT_1:29 ;

then ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(0. X).|| by BHSP_1:30;

then A66: ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + 0 by BHSP_1:26;

||.(setsum Y01).|| < 1 / (k + 1) by A33, A44, A62, A63;

then ||.(setsum Y01).|| < e / 2 by A39, XXREAL_0:2;

then ||.((seq . n) - (seq . m)).|| < e / 2 by A66, XXREAL_0:2;

then ||.((seq . n) - (seq . m)).|| + 0 < (e / 2) + (e / 2) by A36, XREAL_1:8;

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

end;ex Y01 being finite Subset of X st

( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )

proof

then consider Y01 being finite Subset of X such that
take Y01 = Y1 \ Y0; :: thesis: ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )

A61: Y1 \ Y0 c= Y1 by XBOOLE_1:36;

Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39

.= Y1 by A49, XBOOLE_1:12 ;

hence ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A47, A59, A61, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

end;A61: Y1 \ Y0 c= Y1 by XBOOLE_1:36;

Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39

.= Y1 by A49, XBOOLE_1:12 ;

hence ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A47, A59, A61, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

A62: ( not Y01 is empty & Y01 c= Y ) and

A63: Y01 misses Y0 and

A64: Y0 \/ Y01 = Y1 ;

seq . n = (seq . k) + (setsum Y01) by A1, A45, A48, A63, A64, Th2;

then A65: (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 A45, 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 A65, A60, RLVECT_1:29 ;

then ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(0. X).|| by BHSP_1:30;

then A66: ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + 0 by BHSP_1:26;

||.(setsum Y01).|| < 1 / (k + 1) by A33, A44, A62, A63;

then ||.(setsum Y01).|| < e / 2 by A39, XXREAL_0:2;

then ||.((seq . n) - (seq . m)).|| < e / 2 by A66, XXREAL_0:2;

then ||.((seq . n) - (seq . m)).|| + 0 < (e / 2) + (e / 2) by A36, XREAL_1:8;

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

case A67:
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 )

A69: ( not Y02 is empty & Y02 c= Y ) and

A70: Y02 misses Y0 and

A71: Y0 \/ Y02 = Y2 ;

||.(setsum Y02).|| < 1 / (k + 1) by A33, A44, A69, A70;

then A72: ||.(setsum Y02).|| < e / 2 by A39, XXREAL_0:2;

ex Y01 being finite Subset of X st

( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )

A74: ( not Y01 is empty & Y01 c= Y ) and

A75: Y01 misses Y0 and

A76: Y0 \/ Y01 = Y1 ;

setsum Y1 = (setsum Y0) + (setsum Y01) by A1, A75, A76, Th2;

then A77: (seq . n) - (seq . k) = (setsum Y01) + ((seq . k) + (- (seq . k))) by A45, A48, 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, A70, A71, Th2;

then A78: (seq . m) - (seq . k) = (setsum Y02) + ((seq . k) + (- (seq . k))) by A45, A43, 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 A77, A78, RLVECT_1:33 ;

then ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(- (setsum Y02)).|| by BHSP_1:30;

then A79: ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(setsum Y02).|| by BHSP_1:31;

||.(setsum Y01).|| < 1 / (k + 1) by A33, A44, A74, A75;

then ||.(setsum Y01).|| < e / 2 by A39, XXREAL_0:2;

then ||.(setsum Y01).|| + ||.(setsum Y02).|| < (e / 2) + (e / 2) by A72, XREAL_1:8;

hence ||.((seq . n) - (seq . m)).|| < e by A79, XXREAL_0:2; :: thesis: verum

end;( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )

proof

then consider Y02 being finite Subset of X such that
take Y02 = Y2 \ Y0; :: thesis: ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )

A68: Y2 \ Y0 c= Y2 by XBOOLE_1:36;

Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39

.= Y2 by A46, XBOOLE_1:12 ;

hence ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A42, A67, A68, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

end;A68: Y2 \ Y0 c= Y2 by XBOOLE_1:36;

Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39

.= Y2 by A46, XBOOLE_1:12 ;

hence ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A42, A67, A68, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

A69: ( not Y02 is empty & Y02 c= Y ) and

A70: Y02 misses Y0 and

A71: Y0 \/ Y02 = Y2 ;

||.(setsum Y02).|| < 1 / (k + 1) by A33, A44, A69, A70;

then A72: ||.(setsum Y02).|| < e / 2 by A39, 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

then consider Y01 being finite Subset of X such that
take Y01 = Y1 \ Y0; :: thesis: ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )

A73: Y1 \ Y0 c= Y1 by XBOOLE_1:36;

Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39

.= Y1 by A49, XBOOLE_1:12 ;

hence ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A47, A59, A73, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

end;A73: Y1 \ Y0 c= Y1 by XBOOLE_1:36;

Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39

.= Y1 by A49, XBOOLE_1:12 ;

hence ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A47, A59, A73, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

A74: ( not Y01 is empty & Y01 c= Y ) and

A75: Y01 misses Y0 and

A76: Y0 \/ Y01 = Y1 ;

setsum Y1 = (setsum Y0) + (setsum Y01) by A1, A75, A76, Th2;

then A77: (seq . n) - (seq . k) = (setsum Y01) + ((seq . k) + (- (seq . k))) by A45, A48, 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, A70, A71, Th2;

then A78: (seq . m) - (seq . k) = (setsum Y02) + ((seq . k) + (- (seq . k))) by A45, A43, 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 A77, A78, RLVECT_1:33 ;

then ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(- (setsum Y02)).|| by BHSP_1:30;

then A79: ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(setsum Y02).|| by BHSP_1:31;

||.(setsum Y01).|| < 1 / (k + 1) by A33, A44, A74, A75;

then ||.(setsum Y01).|| < e / 2 by A39, XXREAL_0:2;

then ||.(setsum Y01).|| + ||.(setsum Y02).|| < (e / 2) + (e / 2) by A72, XREAL_1:8;

hence ||.((seq . n) - (seq . m)).|| < e by A79, XXREAL_0:2; :: thesis: verum

for n, m being Nat st n >= k & m >= k holds

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

then seq is convergent by BHSP_3:def 4;

then consider x being Point of X such that

A80: for r being Real st r > 0 holds

ex m being Nat st

for n being 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 ) )

hence
Y is summable_set
; :: thesis: verumex 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 A81: 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 ) )

A82: e / 2 > 0 / 2 by A81, XREAL_1:74;

then consider m being Nat such that

A83: for n being Nat st n >= m holds

||.((seq . n) - x).|| < e / 2 by A80;

ex i being Nat st

( 1 / (i + 1) < e / 2 & i >= m )

A85: 1 / (i + 1) < e / 2 and

A86: i >= m ;

reconsider i = i as Element of NAT by ORDINAL1:def 12;

consider Y0 being finite Subset of X such that

A87: not Y0 is empty and

A88: A . i = Y0 and

A89: seq . i = setsum Y0 by A35;

A90: ||.((setsum Y0) - x).|| < e / 2 by A83, A86, A89;

( 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 A87, A88; :: thesis: verum

end;( 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 A81: 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 ) )

A82: e / 2 > 0 / 2 by A81, XREAL_1:74;

then consider m being Nat such that

A83: for n being Nat st n >= m holds

||.((seq . n) - x).|| < e / 2 by A80;

ex i being Nat st

( 1 / (i + 1) < e / 2 & i >= m )

proof

then consider i being Nat such that
set p = e / 2;

consider k1 being Nat such that

A84: (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 A84, XXREAL_0:2;

then ((e / 2) ") + 0 < i + 1 by XREAL_1:8;

then 1 / (i + 1) < 1 / ((e / 2) ") by A82, 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;consider k1 being Nat such that

A84: (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 A84, XXREAL_0:2;

then ((e / 2) ") + 0 < i + 1 by XREAL_1:8;

then 1 / (i + 1) < 1 / ((e / 2) ") by A82, 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

A85: 1 / (i + 1) < e / 2 and

A86: i >= m ;

reconsider i = i as Element of NAT by ORDINAL1:def 12;

consider Y0 being finite Subset of X such that

A87: not Y0 is empty and

A88: A . i = Y0 and

A89: seq . i = setsum Y0 by A35;

A90: ||.((setsum Y0) - x).|| < e / 2 by A83, A86, A89;

now :: thesis: for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

||.(x - (setsum Y1)).|| < e

hence
ex Y0 being finite Subset of X st ||.(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

A91: Y0 c= Y1 and

A92: Y1 c= Y ; :: thesis: ||.(x - (setsum Y1)).|| < e

end;assume that

A91: Y0 c= Y1 and

A92: Y1 c= Y ; :: thesis: ||.(x - (setsum Y1)).|| < e

now :: thesis: ( ( Y0 = Y1 & ||.(x - (setsum Y1)).|| < e ) or ( Y0 <> Y1 & ||.(x - (setsum Y1)).|| < e ) )end;

hence
||.(x - (setsum Y1)).|| < e
; :: thesis: verumper cases
( Y0 = Y1 or Y0 <> Y1 )
;

end;

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 A83, A86, A89;

then ||.(x - (setsum Y1)).|| + 0 < (e / 2) + (e / 2) by A81, XREAL_1:8;

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

end;.= ||.((setsum Y0) - x).|| by RLVECT_1:33 ;

then ||.(x - (setsum Y1)).|| < e / 2 by A83, A86, A89;

then ||.(x - (setsum Y1)).|| + 0 < (e / 2) + (e / 2) by A81, XREAL_1:8;

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

case A93:
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 )

A95: ( not Y2 is empty & Y2 c= Y ) and

A96: Y0 misses Y2 and

A97: Y0 \/ Y2 = Y1 ;

(setsum Y1) - x = ((setsum Y0) + (setsum Y2)) - x by A1, A96, A97, 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 A98: ||.(x + (- (setsum Y1))).|| <= ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| by RLVECT_1:33;

||.(setsum Y2).|| < 1 / (i + 1) by A33, A88, A95, A96;

then ||.(setsum Y2).|| < e / 2 by A85, XXREAL_0:2;

then ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| < (e / 2) + (e / 2) by A90, XREAL_1:8;

hence ||.(x - (setsum Y1)).|| < e by A98, XXREAL_0:2; :: thesis: verum

end;( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 )

proof

then consider Y2 being finite Subset of X such that
take Y2 = Y1 \ Y0; :: thesis: ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 )

A94: Y1 \ Y0 c= Y1 by XBOOLE_1:36;

Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39

.= Y1 by A91, XBOOLE_1:12 ;

hence ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 ) by A92, A93, A94, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

end;A94: Y1 \ Y0 c= Y1 by XBOOLE_1:36;

Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39

.= Y1 by A91, XBOOLE_1:12 ;

hence ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 ) by A92, A93, A94, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum

A95: ( not Y2 is empty & Y2 c= Y ) and

A96: Y0 misses Y2 and

A97: Y0 \/ Y2 = Y1 ;

(setsum Y1) - x = ((setsum Y0) + (setsum Y2)) - x by A1, A96, A97, 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 A98: ||.(x + (- (setsum Y1))).|| <= ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| by RLVECT_1:33;

||.(setsum Y2).|| < 1 / (i + 1) by A33, A88, A95, A96;

then ||.(setsum Y2).|| < e / 2 by A85, XXREAL_0:2;

then ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| < (e / 2) + (e / 2) by A90, XREAL_1:8;

hence ||.(x - (setsum Y1)).|| < e by A98, XXREAL_0:2; :: thesis: verum

( 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 A87, A88; :: thesis: verum

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 ) ) )

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 ) ) )

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

A99: 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 ) ) ;

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;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

A99: 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 ) ) ;

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 ) )

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 ) )

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

A100: not Y0 is empty and

A101: Y0 c= Y and

A102: for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

||.(x - (setsum Y1)).|| < e / 2 by A99, XREAL_1:139;

reconsider Y0 = Y0 as non empty finite Subset of X by A100;

( 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 A101; :: thesis: verum

end;( 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

A100: not Y0 is empty and

A101: Y0 c= Y and

A102: for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

||.(x - (setsum Y1)).|| < e / 2 by A99, XREAL_1:139;

reconsider Y0 = Y0 as non empty finite Subset of X by A100;

now :: thesis: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

||.(setsum Y1).|| < e

hence
ex Y0 being finite Subset of X st ||.(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

A103: Y1 c= Y and

A104: 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 A101, A102, A103, XBOOLE_1:8;

then A105: ||.(x - (setsum (Y0 \/ Y1))).|| + ||.(x - (setsum Y0)).|| < (e / 2) + (e / 2) by A101, A102, XREAL_1:8;

||.((x - (setsum (Y0 \/ Y1))) - (x - (setsum Y0))).|| <= ||.(x - (setsum (Y0 \/ Y1))).|| + ||.(- (x - (setsum Y0))).|| by BHSP_1:30;

then A106: ||.((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, A104, 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 A106, A105, XXREAL_0:2; :: thesis: verum

end;assume that

not Y1 is empty and

A103: Y1 c= Y and

A104: 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 A101, A102, A103, XBOOLE_1:8;

then A105: ||.(x - (setsum (Y0 \/ Y1))).|| + ||.(x - (setsum Y0)).|| < (e / 2) + (e / 2) by A101, A102, XREAL_1:8;

||.((x - (setsum (Y0 \/ Y1))) - (x - (setsum Y0))).|| <= ||.(x - (setsum (Y0 \/ Y1))).|| + ||.(- (x - (setsum Y0))).|| by BHSP_1:30;

then A106: ||.((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, A104, 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 A106, A105, XXREAL_0:2; :: thesis: verum

( 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 A101; :: thesis: verum

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

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