let X be RealUnitarySpace; :: thesis: for Y being Subset of X
for L being Functional of X holds
( Y is_summable_set_by L iff 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
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e ) ) )
let Y be Subset of X; :: thesis: for L being Functional of X holds
( Y is_summable_set_by L iff 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
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e ) ) )
let L be Functional of X; :: thesis: ( Y is_summable_set_by L iff 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
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e ) ) )
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
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e ) ) ) :: 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 not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e ) ) ) implies Y is_summable_set_by L )
proof
assume Y is_summable_set_by L ; :: 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 not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e ) )
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
abs (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
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e ) )
proof
let e be Real; :: thesis: ( 0 < e 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
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e ) ) )
assume A2: 0 < e ; :: 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
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e ) )
consider Y0 being finite Subset of X such that
A3: ( 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 / 2 ) ) by A1, A2, XREAL_1:141;
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e
proof
let Y1 be finite Subset of X; :: thesis: ( not Y1 is empty & Y1 c= Y & Y0 misses Y1 implies abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e )
assume A4: ( not Y1 is empty & Y1 c= Y & Y0 misses Y1 ) ; :: thesis: abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e
set Y1' = Y0 \/ Y1;
( Y0 \/ Y1 = Y0 \/ Y1 & Y0 c= Y0 \/ Y1 & Y0 \/ Y1 c= Y & Y0 \/ Y1 is finite Subset of X ) by A3, A4, XBOOLE_1:7, XBOOLE_1:8;
then abs (r - (setopfunc (Y0 \/ Y1),the carrier of X,REAL ,L,addreal )) < e / 2 by A3;
then A5: abs ((setopfunc (Y0 \/ Y1),the carrier of X,REAL ,L,addreal ) - r) < e / 2 by UNIFORM1:13;
A6: abs (r - (setopfunc Y0,the carrier of X,REAL ,L,addreal )) < e / 2 by A3;
dom L = the carrier of X by FUNCT_2:def 1;
then setopfunc (Y0 \/ Y1),the carrier of X,REAL ,L,addreal = addreal . (setopfunc Y0,the carrier of X,REAL ,L,addreal ),(setopfunc Y1,the carrier of X,REAL ,L,addreal ) by A4, BHSP_5:14
.= (setopfunc Y0,the carrier of X,REAL ,L,addreal ) + (setopfunc Y1,the carrier of X,REAL ,L,addreal ) by BINOP_2:def 9 ;
then setopfunc Y1,the carrier of X,REAL ,L,addreal = (setopfunc (Y0 \/ Y1),the carrier of X,REAL ,L,addreal ) - (setopfunc Y0,the carrier of X,REAL ,L,addreal ) ;
hence abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e by A5, A6, Lm1; :: 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
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e ) ) by A3; :: thesis: verum
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
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e ) ) ; :: thesis: verum
end;
assume A7: 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
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e ) ) ; :: thesis: Y is_summable_set_by L
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
abs (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) )
proof
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
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < 1 / (z + 1) ) );
A8: ex B being Function of NAT ,(bool Y) st
for x being set st x in NAT holds
S1[x,B . x]
proof
now
let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in bool Y & y is finite Subset of X & not y is empty & y 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 & y misses Y1 holds
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < 1 / (z + 1) ) ) )
assume A9: x in NAT ; :: thesis: ex y being set st
( y in bool Y & y is finite Subset of X & not y is empty & y 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 & y misses Y1 holds
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < 1 / (z + 1) ) )
reconsider xx = x as Element of NAT by A9;
reconsider e = 1 / (xx + 1) as Real ;
0 <= xx by NAT_1:2;
then 0 < xx + 1 by NAT_1:13;
then 0 / (xx + 1) < 1 / (xx + 1) by XREAL_1:76;
then consider Y0 being finite Subset of X such that
A10: ( 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
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < e ) ) by A7;
A11: Y0 in bool Y by A10, ZFMISC_1:def 1;
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
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < 1 / (z + 1) by A10;
hence ex y being set st
( y in bool Y & y is finite Subset of X & not y is empty & y 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 & y misses Y1 holds
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < 1 / (z + 1) ) ) by A10, A11; :: thesis: verum
end;
then A12: for x being set st x in NAT holds
ex y being set st
( y in bool Y & S1[x,y] ) ;
thus 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(A12); :: thesis: verum
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
abs (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 Function of NAT ,(bool Y) such that
A13: 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
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < 1 / (z + 1) ) ) by A8;
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
A14: ( dom A = NAT & A . 0 = B . 0 & ( 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
abs (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 ) );
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 A15: 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 );
A16: S3[ 0 ] by A15;
A17: now
let j be Element of NAT ; :: thesis: ( S3[j] implies S3[j + 1] )
assume A18: S3[j] ; :: thesis: S3[j + 1]
A . (j + 1) = (B . (j + 1)) \/ (A . j) by A14;
then A . j c= A . (j + 1) by XBOOLE_1:7;
hence S3[j + 1] by A15, A18, NAT_1:2, XBOOLE_1:1; :: thesis: verum
end;
thus for j being Element of NAT holds S3[j] from NAT_1:sch 1(A16, A17); :: thesis: verum
end;
then A19: S2[ 0 ] by A13, A14;
A20: now
let n be Element of NAT ; :: thesis: ( S2[n] implies S2[n + 1] )
assume A21: S2[n] ; :: thesis: S2[n + 1]
A22: A . (n + 1) = (B . (n + 1)) \/ (A . n) by A14;
A23: B . (n + 1) is finite Subset of X by A13;
A25: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . (n + 1) misses Y1 holds
abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < 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 abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < 1 / ((n + 1) + 1) )
assume A26: ( not Y1 is empty & Y1 c= Y & A . (n + 1) misses Y1 ) ; :: thesis: abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < 1 / ((n + 1) + 1)
A . (n + 1) = (B . (n + 1)) \/ (A . n) by A14;
then ( not Y1 is empty & Y1 c= Y & B . (n + 1) misses Y1 ) by A26, XBOOLE_1:7, XBOOLE_1:63;
hence abs (setopfunc Y1,the carrier of X,REAL ,L,addreal ) < 1 / ((n + 1) + 1) by A13; :: thesis: verum
end;
defpred S3[ Element of NAT ] means ( n + 1 <= $1 implies A . (n + 1) c= A . $1 );
for j being Element of NAT holds S3[j]
proof
A27: S3[ 0 ] by NAT_1:3;
A28: 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
A29: S3[j] and
A30: n + 1 <= j + 1 ; :: thesis: A . (n + 1) c= A . (j + 1)
now
per cases ( n = j or n <> j ) ;
case n = j ; :: thesis: A . (n + 1) c= A . (j + 1)
hence A . (n + 1) c= A . (j + 1) ; :: thesis: verum
end;
case A31: n <> j ; :: thesis: A . (n + 1) c= A . (j + 1)
n <= j by A30, XREAL_1:8;
then A32: n < j by A31, XXREAL_0:1;
A . (j + 1) = (B . (j + 1)) \/ (A . j) by A14;
then A . j c= A . (j + 1) by XBOOLE_1:7;
hence A . (n + 1) c= A . (j + 1) by A29, A32, NAT_1:13, XBOOLE_1:1; :: thesis: verum
end;
end;
end;
hence A . (n + 1) c= A . (j + 1) ; :: thesis: verum
end;
thus for j being Element of NAT holds S3[j] from NAT_1:sch 1(A27, A28); :: thesis: verum
end;
hence S2[n + 1] by A21, A22, A23, A25, XBOOLE_1:8; :: thesis: verum
end;
A33: for i being Element of NAT holds S2[i] from NAT_1:sch 1(A19, A20);
 rng A c= bool Y
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng A or y in bool Y )
assume A34: y in rng A ; :: thesis: y in bool Y
consider x being set such that
A35: ( x in dom A & y = A . x ) by A34, FUNCT_1:def 5;
reconsider i = x as Element of NAT by A14, A35;
A . i c= Y by A33;
hence y in bool Y by A35, ZFMISC_1:def 1; :: thesis: verum
end;
then A is Function of NAT ,(bool Y) by A14, 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
abs (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 A33; :: thesis: verum
end;
then consider A being Function of NAT ,(bool Y) such that
A36: 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
abs (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 S2[ set , set ] 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 );
A37: for x being set st x in NAT holds
ex y being set st
( y in REAL & S2[x,y] )
proof
let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in REAL & S2[x,y] ) )
assume A38: x in NAT ; :: thesis: ex y being set st
( y in REAL & S2[x,y] )
reconsider i = x as Element of NAT by A38;
A39: ( 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
abs (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 A36;
then reconsider Y1 = A . x as finite Subset of X ;
reconsider y = setopfunc Y1,the carrier of X,REAL ,L,addreal as set ;
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 ) by A39;
hence ex y being set st
( y in REAL & S2[x,y] ) ; :: thesis: verum
end;
ex F being Function of NAT ,REAL st
for x being set st x in NAT holds
S2[x,F . x] from FUNCT_2:sch 1(A37);
 then consider F being Function of NAT ,REAL such that
A40: 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 = setopfunc Y1,the carrier of X,REAL ,L,addreal ) ;
set seq = F;
A41: for e being real number st e > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
abs ((F . n) - (F . m)) < e
proof
let e be real number ; :: thesis: ( e > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
abs ((F . n) - (F . m)) < e )
assume A42: e > 0 ; :: thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
abs ((F . n) - (F . m)) < e
A43: e / 2 > 0 / 2 by A42, XREAL_1:76;
then consider k being Element of NAT such that
A44: 1 / (k + 1) < e / 2 by Lm2;
take k ; :: thesis: for n, m being Element of NAT st n >= k & m >= k holds
abs ((F . n) - (F . m)) < e
let n, m be Element of NAT ; :: thesis: ( n >= k & m >= k implies abs ((F . n) - (F . m)) < e )
assume A45: ( n >= k & m >= k ) ; :: thesis: abs ((F . n) - (F . m)) < e
consider Y0 being finite Subset of X such that
A46: ( not Y0 is empty & A . k = Y0 & F . k = setopfunc Y0,the carrier of X,REAL ,L,addreal ) by A40;
consider Y1 being finite Subset of X such that
A47: ( not Y1 is empty & A . n = Y1 & F . n = setopfunc Y1,the carrier of X,REAL ,L,addreal ) by A40;
consider Y2 being finite Subset of X such that
A48: ( not Y2 is empty & A . m = Y2 & F . m = setopfunc Y2,the carrier of X,REAL ,L,addreal ) by A40;
A49: Y0 c= Y1 by A36, A45, A46, A47;
A50: Y0 c= Y2 by A36, A45, A46, A48;
now
per cases ( Y0 = Y1 or Y0 <> Y1 ) ;
case A51: Y0 = Y1 ; :: thesis: abs ((F . n) - (F . m)) < e
now
per cases ( Y0 = Y2 or Y0 <> Y2 ) ;
case Y0 = Y2 ; :: thesis: abs ((F . n) - (F . m)) < e
hence abs ((F . n) - (F . m)) < e by A42, A47, A48, A51, ABSVALUE:7; :: thesis: verum
end;
case A52: Y0 <> Y2 ; :: thesis: abs ((F . n) - (F . 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 )
A53: Y2 \ Y0 c= Y2 by XBOOLE_1:36;
Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
.= Y2 by A50, XBOOLE_1:12 ;
hence ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A48, A52, A53, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum
end;
then consider Y02 being finite Subset of X such that
A54: ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) ;
dom L = the carrier of X by FUNCT_2:def 1;
then A55: 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 A54, 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 ;
abs (setopfunc Y02,the carrier of X,REAL ,L,addreal ) < 1 / (k + 1) by A36, A46, A54;
then A56: abs (setopfunc Y02,the carrier of X,REAL ,L,addreal ) < e / 2 by A44, XXREAL_0:2;
A57: abs ((F . n) - (F . m)) = abs (- (setopfunc Y02,the carrier of X,REAL ,L,addreal )) by A47, A48, A51, A55
.= abs (setopfunc Y02,the carrier of X,REAL ,L,addreal ) by COMPLEX1:138 ;
e / 2 < e by A42, XREAL_1:218;
hence abs ((F . n) - (F . m)) < e by A56, A57, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence abs ((F . n) - (F . m)) < e ; :: thesis: verum
end;
case A58: Y0 <> Y1 ; :: thesis: abs ((F . n) - (F . m)) < e
now
per cases ( Y0 = Y2 or Y0 <> Y2 ) ;
case A59: Y0 = Y2 ; :: thesis: abs ((F . n) - (F . m)) < e
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 )
A60: 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, A58, A60, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum
end;
then consider Y01 being finite Subset of X such that
A61: ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) ;
dom L = the carrier of X by FUNCT_2:def 1;
then A62: 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 A61, 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 ;
abs (setopfunc Y01,the carrier of X,REAL ,L,addreal ) < 1 / (k + 1) by A36, A46, A61;
then abs ((F . n) - (F . m)) < e / 2 by A44, A47, A48, A59, A62, XXREAL_0:2;
then (abs ((F . n) - (F . m))) + 0 < (e / 2) + (e / 2) by A43, XREAL_1:10;
hence abs ((F . n) - (F . m)) < e ; :: thesis: verum
end;
case A63: Y0 <> Y2 ; :: thesis: abs ((F . n) - (F . m)) < e
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 )
A64: 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, A58, A64, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum
end;
then consider Y01 being finite Subset of X such that
A65: ( 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: ( 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 A50, XBOOLE_1:12 ;
hence ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A48, A63, 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 & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) ;
abs (setopfunc Y01,the carrier of X,REAL ,L,addreal ) < 1 / (k + 1) by A36, A46, A65;
then A68: abs (setopfunc Y01,the carrier of X,REAL ,L,addreal ) < e / 2 by A44, XXREAL_0:2;
abs (setopfunc Y02,the carrier of X,REAL ,L,addreal ) < 1 / (k + 1) by A36, A46, A67;
then abs (setopfunc Y02,the carrier of X,REAL ,L,addreal ) < e / 2 by A44, XXREAL_0:2;
then A69: (abs (setopfunc Y01,the carrier of X,REAL ,L,addreal )) + (abs (setopfunc Y02,the carrier of X,REAL ,L,addreal )) < (e / 2) + (e / 2) by A68, XREAL_1:10;
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 A65, 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 ;
dom L = the carrier of X by FUNCT_2:def 1;
then 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 A67, 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 ;
then (F . n) - (F . m) = (setopfunc Y01,the carrier of X,REAL ,L,addreal ) - (setopfunc Y02,the carrier of X,REAL ,L,addreal ) by A47, A48, A70;
then abs ((F . n) - (F . m)) <= (abs (setopfunc Y01,the carrier of X,REAL ,L,addreal )) + (abs (setopfunc Y02,the carrier of X,REAL ,L,addreal )) by COMPLEX1:143;
hence abs ((F . n) - (F . m)) < e by A69, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence abs ((F . n) - (F . m)) < e ; :: thesis: verum
end;
end;
end;
hence abs ((F . n) - (F . m)) < e ; :: thesis: verum
end;
for e being real number st 0 < e holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((F . m) - (F . k)) < e
proof
let e be real number ; :: thesis: ( 0 < e implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((F . m) - (F . k)) < e )
assume A71: 0 < e ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((F . m) - (F . k)) < e
consider k being Element of NAT such that
A72: for n, m being Element of NAT st n >= k & m >= k holds
abs ((F . n) - (F . m)) < e by A41, A71;
for m being Element of NAT st k <= m holds
abs ((F . m) - (F . k)) < e by A72;
hence ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((F . m) - (F . k)) < e ; :: thesis: verum
end;
then F is convergent by SEQ_4:58;
then consider x being real number such that
A73: for r being real number st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
abs ((F . n) - x) < r by SEQ_2:def 6;
reconsider r = x as Real by XREAL_0:def 1;
A74: 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
abs (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) )
proof
let e be Real; :: thesis: ( 0 < e 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 (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) )
assume A75: 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 (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) )
A76: e / 2 > 0 / 2 by A75, XREAL_1:76;
then consider m being Element of NAT such that
A77: for n being Element of NAT st n >= m holds
abs ((F . n) - r) < e / 2 by A73;
consider i being Element of NAT such that
A78: ( 1 / (i + 1) < e / 2 & i >= m ) by A76, Lm3;
consider Y0 being finite Subset of X such that
A79: ( not Y0 is empty & A . i = Y0 & F . i = setopfunc Y0,the carrier of X,REAL ,L,addreal ) by A40;
A80: abs ((setopfunc Y0,the carrier of X,REAL ,L,addreal ) - r) < e / 2 by A77, A78, A79;
now
let Y1 be finite Subset of X; :: thesis: ( Y0 c= Y1 & Y1 c= Y implies abs (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e )
assume A81: ( Y0 c= Y1 & Y1 c= Y ) ; :: thesis: abs (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e
now
per cases ( Y0 = Y1 or Y0 <> Y1 ) ;
case Y0 = Y1 ; :: thesis: abs (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e
then abs (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e / 2 by A80, UNIFORM1:13;
then (abs (x - (setopfunc Y1,the carrier of X,REAL ,L,addreal ))) + 0 < (e / 2) + (e / 2) by A76, XREAL_1:10;
hence abs (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ; :: thesis: verum
end;
case A82: Y0 <> Y1 ; :: thesis: abs (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < 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 )
A83: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A81, XBOOLE_1:12 ;
hence ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 ) by A81, A82, A83, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum
end;
then consider Y2 being finite Subset of X such that
A84: ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 ) ;
abs (setopfunc Y2,the carrier of X,REAL ,L,addreal ) < 1 / (i + 1) by A36, A79, A84;
then A85: abs (setopfunc Y2,the carrier of X,REAL ,L,addreal ) < e / 2 by A78, XXREAL_0:2;
dom L = the carrier of X by FUNCT_2:def 1;
then (setopfunc Y1,the carrier of X,REAL ,L,addreal ) - r = (addreal . (setopfunc Y0,the carrier of X,REAL ,L,addreal ),(setopfunc Y2,the carrier of X,REAL ,L,addreal )) - r by A84, BHSP_5:14
.= ((setopfunc Y0,the carrier of X,REAL ,L,addreal ) + (setopfunc Y2,the carrier of X,REAL ,L,addreal )) - r by BINOP_2:def 9
.= ((setopfunc Y0,the carrier of X,REAL ,L,addreal ) - r) + (setopfunc Y2,the carrier of X,REAL ,L,addreal ) ;
then abs ((setopfunc Y1,the carrier of X,REAL ,L,addreal ) - r) <= (abs ((setopfunc Y0,the carrier of X,REAL ,L,addreal ) - r)) + (abs (setopfunc Y2,the carrier of X,REAL ,L,addreal )) by ABSVALUE:21;
then A86: abs (x - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) <= (abs ((setopfunc Y0,the carrier of X,REAL ,L,addreal ) - r)) + (abs (setopfunc Y2,the carrier of X,REAL ,L,addreal )) by UNIFORM1:13;
(abs ((setopfunc Y0,the carrier of X,REAL ,L,addreal ) - r)) + (abs (setopfunc Y2,the carrier of X,REAL ,L,addreal )) < (e / 2) + (e / 2) by A80, A85, XREAL_1:10;
hence abs (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e by A86, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence abs (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < 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
abs (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) by A79; :: thesis: verum
end;
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
abs (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) )
thus 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
abs (r - (setopfunc Y1,the carrier of X,REAL ,L,addreal )) < e ) ) by A74; :: thesis: verum
end;
hence Y is_summable_set_by L by BHSP_6:def 6; :: thesis: verum