let X be RealUnitarySpace; :: thesis:
let Y be Subset of X; :: thesis:
let L be Functional of X; :: thesis:
thus ( Y is_summable_set_by L implies 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 not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) ) :: thesis:

assume Y is_summable_set_by L ; :: thesis:
then consider r being Real such that
A1: 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
|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) by BHSP_6:def 6;
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 not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) )

let e be Real; :: thesis:
assume 0 < e ; :: thesis:
then consider Y0 being finite Subset of X such that
A2: not Y0 is empty and
A3: Y0 c= Y and
A4: for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e / 2 by A1, XREAL_1:139;
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e

proof

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
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) by A2, A3; :: thesis:

end;

hence 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 not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) ; :: thesis:

end;

assume A9: 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 not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) ; :: thesis:
ex r being Real st
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
|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )

proof

defpred S₁[ 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
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) );
A10: for x being object st x in NAT holds
ex y being object st
( y in bool Y & S₁[x,y] )

proof

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider xx = x as Element of 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
A11: not Y0 is empty and
A12: ( Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < e ) ) by A9;
take Y0 ; :: thesis:
thus Y0 in bool Y by A12, ZFMISC_1:def 1; :: thesis:
take D2 = Y0; :: thesis:
thus D2 = Y0 ; :: thesis:
thus Y0 is finite Subset of X ; :: thesis:
thus not D2 is empty by A11; :: thesis:
thus D2 c= Y by A12; :: thesis:
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
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) by A12;
hence for z being Real st z = x holds
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & D2 misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ; :: thesis:

end;

A13: ex B being sequence of (bool Y) st
for x being object st x in NAT holds
S₁[x,B . x] from FUNCT_2:sch 1(A10);
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
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds
A . i c= A . j ) )

proof

consider B being sequence of (bool Y) such that
A14: for x being object st x in NAT holds
S₁[x,B . x] by A13;
A15: 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
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) )

proof

let x be object ; :: thesis:
assume A16: x in NAT ; :: thesis:
S₁[x,B . x] by A16, A14;
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
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (z + 1) ) ) ; :: thesis:

end;

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
A17: dom A = NAT and
A18: A . 0 = B . 0 and
A19: for n being Nat holds A . (n + 1) = (B . (n + 1)) \/ (A . n) ;
defpred S₂[ 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
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / ($1 + 1) ) & ( for j being Element of NAT st $1 <= j holds
A . $1 c= A . j ) );

A20: now :: thesis:

let n be Nat; :: thesis:
assume A21: S₂[n] ; :: thesis:
A22: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . (n + 1) misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / ((n + 1) + 1)

proof

let Y1 be finite Subset of X; :: thesis:
assume that
A23: ( not Y1 is empty & Y1 c= Y ) and
A24: A . (n + 1) misses Y1 ; :: thesis:
A . (n + 1) = (B . (n + 1)) \/ (A . n) by A19;
then B . (n + 1) misses Y1 by A24, XBOOLE_1:7, XBOOLE_1:63;
hence |.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / ((n + 1) + 1) by A15, A23; :: thesis:

end;

defpred S₃[ Nat] means ( n + 1 <= $1 implies A . (n + 1) c= A . $1 );
A25: for j being Nat st S₃[j] holds
S₃[j + 1]

proof

let j be Nat; :: thesis:
assume that
A26: S₃[j] and
A27: n + 1 <= j + 1 ; :: thesis:

now :: thesis:

per cases ;

case n = j ; :: thesis:

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

end;

case A28: n <> j ; :: thesis:

A . (j + 1) = (B . (j + 1)) \/ (A . j) by A19;
then A29: A . j c= A . (j + 1) by XBOOLE_1:7;
n <= j by A27, XREAL_1:6;
then n < j by A28, XXREAL_0:1;
hence A . (n + 1) c= A . (j + 1) by A26, A29, NAT_1:13; :: thesis:

end;

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

end;

A30: S₃[ 0 ] ;
A31: for j being Nat holds S₃[j] from NAT_1:sch 2(A30, A25);
( A . (n + 1) = (B . (n + 1)) \/ (A . n) & B . (n + 1) is finite Subset of X ) by A15, A19;
hence S₂[n + 1] by A21, A22, A31, XBOOLE_1:8; :: thesis:

end;

for j0 being Nat st j0 = 0 holds
for j being Nat st j0 <= j holds
A . j0 c= A . j

proof

let j0 be Nat; :: thesis:
assume A32: j0 = 0 ; :: thesis:
defpred S₃[ Nat] means ( j0 <= $1 implies A . j0 c= A . $1 );

A33: now :: thesis:

let j be Nat; :: thesis:
assume A34: S₃[j] ; :: thesis:
A . (j + 1) = (B . (j + 1)) \/ (A . j) by A19;
then A . j c= A . (j + 1) by XBOOLE_1:7;
hence S₃[j + 1] by A32, A34, XBOOLE_1:1; :: thesis:

end;

A35: S₃[ 0 ] by A32;
thus for j being Nat holds S₃[j] from NAT_1:sch 2(A35, A33); :: thesis:

end;

then A36: S₂[ 0 ] by A15, A18;
A37: for i being Nat holds S₂[i] from NAT_1:sch 2(A36, A20);
rng A c= bool Y

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng A ; :: thesis:
then consider x being object such that
A38: x in dom A and
A39: y = A . x by FUNCT_1:def 3;
reconsider i = x as Element of NAT by A17, A38;
A . i c= Y by A37;
hence y in bool Y by A39, ZFMISC_1:def 1; :: thesis:

end;

then A is sequence of (bool Y) by A17, 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
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds
A . i c= A . j ) ) by A37; :: thesis:

end;

then consider A being sequence of (bool Y) such that
A40: 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
|.(setopfunc (Y1, the carrier of X,REAL,L,addreal)).| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds
A . i c= A . j ) ) ;
defpred S₂[ object , object ] means ex Y1 being finite Subset of X st
( not Y1 is empty & A . $1 = Y1 & $2 = setopfunc (Y1, the carrier of X,REAL,L,addreal) );
A41: for x being object st x in NAT holds
ex y being object st
( y in REAL & S₂[x,y] )

proof

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider i = x as Element of NAT ;
A . i is finite Subset of X by A40;
then reconsider Y1 = A . x as finite Subset of X ;
reconsider y = setopfunc (Y1, the carrier of X,REAL,L,addreal) as set ;
not A . i is empty by A40;
then ex Y1 being finite Subset of X st
( not Y1 is empty & A . x = Y1 & y = setopfunc (Y1, the carrier of X,REAL,L,addreal) ) ;
hence ex y being object st
( y in REAL & S₂[x,y] ) ; :: thesis:

end;

ex F being sequence of REAL st
for x being object st x in NAT holds
S₂[x,F . x] from FUNCT_2:sch 1(A41);
then consider F being sequence of REAL such that
A42: 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 = setopfunc (Y1, the carrier of X,REAL,L,addreal) ) ;
set seq = F;
A43: for e being Real st e > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
|.((F . n) - (F . m)).| < e

proof

let e be Real; :: thesis:
assume A44: e > 0 ; :: thesis:
A45: e / 2 > 0 / 2 by A44, XREAL_1:74;
then consider k being Nat such that
A46: 1 / (k + 1) < e / 2 by Lm2;
take k ; :: thesis:
let nn, mm be Nat; :: thesis:
assume that
A47: nn >= k and
A48: mm >= k ; :: thesis:
reconsider m = mm, n = nn, k = k as Element of NAT by ORDINAL1:def 12;
consider Y2 being finite Subset of X such that
not Y2 is empty and
A49: A . m = Y2 and
A50: F . m = setopfunc (Y2, the carrier of X,REAL,L,addreal) by A42;
consider Y0 being finite Subset of X such that
not Y0 is empty and
A51: A . k = Y0 and
F . k = setopfunc (Y0, the carrier of X,REAL,L,addreal) by A42;
A52: Y0 c= Y2 by A40, A48, A51, A49;
consider Y1 being finite Subset of X such that
not Y1 is empty and
A53: A . n = Y1 and
A54: F . n = setopfunc (Y1, the carrier of X,REAL,L,addreal) by A42;
A55: Y0 c= Y1 by A40, A47, A51, A53;

now :: thesis:

per cases ;

case A56: Y0 = Y1 ; :: thesis:

now :: thesis:

per cases ;

case Y0 = Y2 ; :: thesis:

hence |.((F . nn) - (F . mm)).| < e by A44, A54, A50, A56, ABSVALUE:2; :: thesis:

end;

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

end;

end;

hence |.((F . nn) - (F . mm)).| < e ; :: thesis:

end;

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

now :: thesis:

per cases ;

case A65: 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:
A66: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A55, XBOOLE_1:12 ;
hence ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A53, A64, A66, XBOOLE_1:1, XBOOLE_1:79; :: thesis:

end;

then consider Y01 being finite Subset of X such that
A67: ( not Y01 is empty & Y01 c= Y ) and
A68: Y01 misses Y0 and
A69: Y0 \/ Y01 = Y1 ;
dom L = the carrier of X by FUNCT_2:def 1;
then A70: setopfunc (Y1, the carrier of X,REAL,L,addreal) = addreal . ((setopfunc (Y0, the carrier of X,REAL,L,addreal)),(setopfunc (Y01, the carrier of X,REAL,L,addreal))) by A68, A69, BHSP_5:14
.= (setopfunc (Y0, the carrier of X,REAL,L,addreal)) + (setopfunc (Y01, the carrier of X,REAL,L,addreal)) by BINOP_2:def 9 ;
|.(setopfunc (Y01, the carrier of X,REAL,L,addreal)).| < 1 / (k + 1) by A40, A51, A67, A68;
then |.((F . n) - (F . m)).| < e / 2 by A46, A54, A50, A65, A70, XXREAL_0:2;
then |.((F . n) - (F . m)).| + 0 < (e / 2) + (e / 2) by A45, XREAL_1:8;
hence |.((F . nn) - (F . mm)).| < e ; :: thesis:

end;

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

end;

then consider Y02 being finite Subset of X such that
A73: ( not Y02 is empty & Y02 c= Y ) and
A74: Y02 misses Y0 and
A75: Y0 \/ Y02 = Y2 ;
dom L = the carrier of X by FUNCT_2:def 1;
then A76: setopfunc (Y2, the carrier of X,REAL,L,addreal) = addreal . ((setopfunc (Y0, the carrier of X,REAL,L,addreal)),(setopfunc (Y02, the carrier of X,REAL,L,addreal))) by A74, A75, BHSP_5:14
.= (setopfunc (Y0, the carrier of X,REAL,L,addreal)) + (setopfunc (Y02, the carrier of X,REAL,L,addreal)) by BINOP_2:def 9 ;
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:
A77: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A55, XBOOLE_1:12 ;
hence ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A53, A64, A77, XBOOLE_1:1, XBOOLE_1:79; :: thesis:

end;

end;

hence |.((F . nn) - (F . mm)).| < e ; :: thesis:

end;

hence |.((F . nn) - (F . mm)).| < e ; :: thesis:

end;

for e being Real st 0 < e holds
ex k being Nat st
for m being Nat st k <= m holds
|.((F . m) - (F . k)).| < e

proof

let e be Real; :: thesis:
assume 0 < e ; :: thesis:
then consider k being Nat such that
A83: for n, m being Nat st n >= k & m >= k holds
|.((F . n) - (F . m)).| < e by A43;
for m being Nat st k <= m holds
|.((F . m) - (F . k)).| < e by A83;
hence ex k being Nat st
for m being Nat st k <= m holds
|.((F . m) - (F . k)).| < e ; :: thesis:

end;

then F is convergent by SEQ_4:41;
then consider x being Real such that
A84: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
|.((F . n) - x).| < r by SEQ_2:def 6;
reconsider r = x as Real ;
take r ; :: thesis:
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
|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )

proof

let e be Real; :: thesis:
assume e > 0 ; :: thesis:
then A85: e / 2 > 0 / 2 by XREAL_1:74;
then consider m being Nat such that
A86: for n being Nat st n >= m holds
|.((F . n) - r).| < e / 2 by A84;
consider i being Nat such that
A87: 1 / (i + 1) < e / 2 and
A88: i >= m by A85, Lm3;
i in NAT by ORDINAL1:def 12;
then reconsider ii = i as Element of NAT ;
consider Y0 being finite Subset of X such that
A89: not Y0 is empty and
A90: A . ii = Y0 and
A91: F . i = setopfunc (Y0, the carrier of X,REAL,L,addreal) by A42;
A92: |.((setopfunc (Y0, the carrier of X,REAL,L,addreal)) - r).| < e / 2 by A86, A88, A91;

now :: thesis:

let Y1 be finite Subset of X; :: thesis:
assume that
A93: Y0 c= Y1 and
A94: Y1 c= Y ; :: thesis:

now :: thesis:

per cases ;

case Y0 = Y1 ; :: thesis:

end;

case A95: 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:
A96: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A93, XBOOLE_1:12 ;
hence ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 ) by A94, A95, A96, XBOOLE_1:79; :: thesis:

end;

end;

hence |.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < 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
|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) by A89, A90; :: thesis:

end;

hence 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
|.(r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) ; :: thesis:

end;

hence Y is_summable_set_by L by BHSP_6:def 6; :: thesis: