let X be RealHilbertSpace; :: thesis: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity implies for Y being Subset of X holds
( Y is summable_set iff for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) ) )
assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity ) ; :: thesis: for Y being Subset of X holds
( Y is summable_set iff for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) )
let Y be Subset of X; :: thesis: ( Y is summable_set iff for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) )
A2: now
defpred S1[ set , set ] means ( $2 is finite Subset of X & not $2 is empty & $2 c= Y & ( for z being Real st z = $1 holds
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & $2 misses Y1 holds
||.(setsum Y1).|| < 1 / (z + 1) ) );
assume A3: for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) ; :: thesis: Y is summable_set
A4: now
let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in bool Y & S1[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in bool Y & S1[x,y] )
then reconsider xx = x as Element of NAT ;
reconsider e = 1 / (xx + 1) as Real by XREAL_0:def 1;
0 / (xx + 1) < 1 / (xx + 1) by XREAL_1:74;
then consider Y0 being finite Subset of X such that
A5: ( not Y0 is empty & Y0 c= Y ) and
A6: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e by A3;
for z being Real st z = x holds
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < 1 / (z + 1) by A6;
hence ex y being set st
( y in bool Y & S1[x,y] ) by A5; :: thesis: verum
end;
A7: ex B being Function of NAT,(bool Y) st
for x being set st x in NAT holds
S1[x,B . x] from FUNCT_2:sch 1(A4);
 ex A being Function of NAT,(bool Y) st
for i being Element of NAT holds
( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds
||.(setsum Y1).|| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds
A . i c= A . j ) )
proof
consider B being Function of NAT,(bool Y) such that
A8: for x being set st x in NAT holds
( B . x is finite Subset of X & not B . x is empty & B . x c= Y & ( for z being Real st z = x holds
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & B . x misses Y1 holds
||.(setsum Y1).|| < 1 / (z + 1) ) ) by A7;
deffunc H1( Nat, set ) -> set = (B . ($1 + 1)) \/ $2;
ex A being Function st
( dom A = NAT & A . 0 = B . 0 & ( for n being Nat holds A . (n + 1) = H1(n,A . n) ) ) from NAT_1:sch 11();
 then consider A being Function such that
A9: dom A = NAT and
A10: A . 0 = B . 0 and
A11: for n being Nat holds A . (n + 1) = (B . (n + 1)) \/ (A . n) ;
defpred S2[ Element of NAT ] means ( A . $1 is finite Subset of X & not A . $1 is empty & A . $1 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . $1 misses Y1 holds
||.(setsum Y1).|| < 1 / ($1 + 1) ) & ( for j being Element of NAT st $1 <= j holds
A . $1 c= A . j ) );
A12: now
let n be Element of NAT ; :: thesis: ( S2[n] implies S2[n + 1] )
assume A13: S2[n] ; :: thesis: S2[n + 1]
A14: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . (n + 1) misses Y1 holds
||.(setsum Y1).|| < 1 / ((n + 1) + 1)
proof
let Y1 be finite Subset of X; :: thesis: ( not Y1 is empty & Y1 c= Y & A . (n + 1) misses Y1 implies ||.(setsum Y1).|| < 1 / ((n + 1) + 1) )
assume that
A15: ( not Y1 is empty & Y1 c= Y ) and
A16: A . (n + 1) misses Y1 ; :: thesis: ||.(setsum Y1).|| < 1 / ((n + 1) + 1)
A . (n + 1) = (B . (n + 1)) \/ (A . n) by A11;
then B . (n + 1) misses Y1 by A16, XBOOLE_1:7, XBOOLE_1:63;
hence ||.(setsum Y1).|| < 1 / ((n + 1) + 1) by A8, A15; :: thesis: verum
end;
defpred S3[ Element of NAT ] means ( n + 1 <= $1 implies A . (n + 1) c= A . $1 );
A17: for j being Element of NAT st S3[j] holds
S3[j + 1]
proof
let j be Element of NAT ; :: thesis: ( S3[j] implies S3[j + 1] )
assume that
A18: ( n + 1 <= j implies A . (n + 1) c= A . j ) and
A19: n + 1 <= j + 1 ; :: thesis: A . (n + 1) c= A . (j + 1)
per cases ( n = j or n <> j ) ;
suppose n = j ; :: thesis: A . (n + 1) c= A . (j + 1)
hence A . (n + 1) c= A . (j + 1) ; :: thesis: verum
end;
suppose A20: n <> j ; :: thesis: A . (n + 1) c= A . (j + 1)
A . (j + 1) = (B . (j + 1)) \/ (A . j) by A11;
then A21: A . j c= A . (j + 1) by XBOOLE_1:7;
n <= j by A19, XREAL_1:6;
then n < j by A20, XXREAL_0:1;
hence A . (n + 1) c= A . (j + 1) by A18, A21, NAT_1:13, XBOOLE_1:1; :: thesis: verum
end;
end;
end;
A22: S3[ 0 ] ;
A23: for j being Element of NAT holds S3[j] from NAT_1:sch 1(A22, A17);
 ( A . (n + 1) = (B . (n + 1)) \/ (A . n) & B . (n + 1) is finite Subset of X ) by A8, A11;
hence S2[n + 1] by A13, A14, A23, XBOOLE_1:8; :: thesis: verum
end;
for j0 being Element of NAT st j0 = 0 holds
for j being Element of NAT st j0 <= j holds
A . j0 c= A . j
proof
let j0 be Element of NAT ; :: thesis: ( j0 = 0 implies for j being Element of NAT st j0 <= j holds
A . j0 c= A . j )
assume A24: j0 = 0 ; :: thesis: for j being Element of NAT st j0 <= j holds
A . j0 c= A . j
defpred S3[ Element of NAT ] means ( j0 <= $1 implies A . j0 c= A . $1 );
A25: now
let j be Element of NAT ; :: thesis: ( S3[j] implies S3[j + 1] )
assume A26: S3[j] ; :: thesis: S3[j + 1]
A . (j + 1) = (B . (j + 1)) \/ (A . j) by A11;
then A . j c= A . (j + 1) by XBOOLE_1:7;
hence S3[j + 1] by A24, A26, XBOOLE_1:1; :: thesis: verum
end;
A27: S3[ 0 ] ;
thus for j being Element of NAT holds S3[j] from NAT_1:sch 1(A27, A25); :: thesis: verum
end;
then A28: S2[ 0 ] by A8, A10;
A29: for i being Element of NAT holds S2[i] from NAT_1:sch 1(A28, A12);
now
let y be set ; :: thesis: ( y in rng A implies y in bool Y )
assume y in rng A ; :: thesis: y in bool Y
then consider x being set such that
A30: x in dom A and
A31: y = A . x by FUNCT_1:def 3;
reconsider i = x as Element of NAT by A9, A30;
A . i c= Y by A29;
hence y in bool Y by A31; :: thesis: verum
end;
then rng A c= bool Y by TARSKI:def 3;
then A is Function of NAT,(bool Y) by A9, FUNCT_2:2;
hence ex A being Function of NAT,(bool Y) st
for i being Element of NAT holds
( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds
||.(setsum Y1).|| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds
A . i c= A . j ) ) by A29; :: thesis: verum
end;
then consider A being Function of NAT,(bool Y) such that
A32: for i being Element of NAT holds
( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds
||.(setsum Y1).|| < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds
A . i c= A . j ) ) ;
defpred S2[ set , set ] means ex Y1 being finite Subset of X st
( not Y1 is empty & A . $1 = Y1 & $2 = setsum Y1 );
A33: for x being set st x in NAT holds
ex y being set st
( y in the carrier of X & S2[x,y] )
proof
let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in the carrier of X & S2[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in the carrier of X & S2[x,y] )
then reconsider i = x as Element of NAT ;
A . i is finite Subset of X by A32;
then reconsider Y1 = A . x as finite Subset of X ;
reconsider y = setsum Y1 as set ;
not A . i is empty by A32;
then ex Y1 being finite Subset of X st
( Y1 is non empty set & A . x = Y1 & y = setsum Y1 ) ;
hence ex y being set st
( y in the carrier of X & S2[x,y] ) ; :: thesis: verum
end;
ex F being Function of NAT, the carrier of X st
for x being set st x in NAT holds
S2[x,F . x] from FUNCT_2:sch 1(A33);
then consider F being Function of NAT, the carrier of X such that
A34: for x being set st x in NAT holds
ex Y1 being finite Subset of X st
( not Y1 is empty & A . x = Y1 & F . x = setsum Y1 ) ;
reconsider seq = F as sequence of X ;
now
let e be Real; :: thesis: ( e > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < e )
assume A35: e > 0 ; :: thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < e
A36: e / 2 > 0 / 2 by A35, XREAL_1:74;
ex k being Element of NAT st 1 / (k + 1) < e / 2
proof
set p = e / 2;
consider k1 being Element of NAT such that
A37: (e / 2) " < k1 by SEQ_4:3;
take k = k1; :: thesis: 1 / (k + 1) < e / 2
((e / 2) ") + 0 < k1 + 1 by A37, XREAL_1:8;
then 1 / (k1 + 1) < 1 / ((e / 2) ") by A36, XREAL_1:76;
then 1 / (k + 1) < 1 * (((e / 2) ") ") by XCMPLX_0:def 9;
hence 1 / (k + 1) < e / 2 ; :: thesis: verum
end;
then consider k being Element of NAT such that
A38: 1 / (k + 1) < e / 2 ;
now
let n, m be Element of NAT ; :: thesis: ( n >= k & m >= k implies ||.((seq . n) - (seq . m)).|| < e )
assume that
A39: n >= k and
A40: m >= k ; :: thesis: ||.((seq . n) - (seq . m)).|| < e
consider Y2 being finite Subset of X such that
not Y2 is empty and
A41: A . m = Y2 and
A42: seq . m = setsum Y2 by A34;
consider Y0 being finite Subset of X such that
not Y0 is empty and
A43: A . k = Y0 and
A44: seq . k = setsum Y0 by A34;
A45: Y0 c= Y2 by A32, A40, A43, A41;
consider Y1 being finite Subset of X such that
not Y1 is empty and
A46: A . n = Y1 and
A47: seq . n = setsum Y1 by A34;
A48: Y0 c= Y1 by A32, A39, A43, A46;
now
per cases ( Y0 = Y1 or Y0 <> Y1 ) ;
case A49: Y0 = Y1 ; :: thesis: ||.((seq . n) - (seq . m)).|| < e
now
per cases ( Y0 = Y2 or Y0 <> Y2 ) ;
case Y0 = Y2 ; :: thesis: ||.((seq . n) - (seq . m)).|| < e
then (seq . n) - (seq . m) = 0. X by A47, A42, A49, RLVECT_1:5;
hence ||.((seq . n) - (seq . m)).|| < e by A35, BHSP_1:26; :: thesis: verum
end;
case A50: Y0 <> Y2 ; :: thesis: ||.((seq . n) - (seq . m)).|| < e
ex Y02 being finite Subset of X st
( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )
proof
take Y02 = Y2 \ Y0; :: thesis: ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )
A51: Y2 \ Y0 c= Y2 by XBOOLE_1:36;
Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
.= Y2 by A45, XBOOLE_1:12 ;
hence ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A41, A50, A51, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum
end;
then consider Y02 being finite Subset of X such that
A52: ( not Y02 is empty & Y02 c= Y ) and
A53: Y02 misses Y0 and
A54: Y0 \/ Y02 = Y2 ;
||.(setsum Y02).|| < 1 / (k + 1) by A32, A43, A52, A53;
then A55: ||.(setsum Y02).|| < e / 2 by A38, XXREAL_0:2;
setsum Y2 = (setsum Y0) + (setsum Y02) by A1, A53, A54, Th2;
then A56: ||.((seq . n) - (seq . m)).|| = ||.(((setsum Y0) - (setsum Y0)) - (setsum Y02)).|| by A47, A42, A49, RLVECT_1:27
.= ||.((0. X) - (setsum Y02)).|| by RLVECT_1:15
.= ||.(- (setsum Y02)).|| by RLVECT_1:14
.= ||.(setsum Y02).|| by BHSP_1:31 ;
e * (1 / 2) < e * 1 by A35, XREAL_1:68;
hence ||.((seq . n) - (seq . m)).|| < e by A55, A56, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence ||.((seq . n) - (seq . m)).|| < e ; :: thesis: verum
end;
case A57: Y0 <> Y1 ; :: thesis: ||.((seq . n) - (seq . m)).|| < e
now
per cases ( Y0 = Y2 or Y0 <> Y2 ) ;
case Y0 = Y2 ; :: thesis: ||.((seq . n) - (seq . m)).|| < e
then A58: (seq . k) - (seq . m) = 0. X by A44, A42, RLVECT_1:5;
ex Y01 being finite Subset of X st
( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )
proof
take Y01 = Y1 \ Y0; :: thesis: ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )
A59: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A48, XBOOLE_1:12 ;
hence ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A46, A57, A59, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum
end;
then consider Y01 being finite Subset of X such that
A60: ( not Y01 is empty & Y01 c= Y ) and
A61: Y01 misses Y0 and
A62: Y0 \/ Y01 = Y1 ;
seq . n = (seq . k) + (setsum Y01) by A1, A44, A47, A61, A62, Th2;
then A63: (seq . n) - (seq . k) = (seq . k) + ((setsum Y01) + (- (seq . k))) by RLVECT_1:def 3
.= (seq . k) - ((seq . k) - (setsum Y01)) by RLVECT_1:33
.= ((setsum Y0) - (setsum Y0)) + (setsum Y01) by A44, RLVECT_1:29
.= (0. X) + (setsum Y01) by RLVECT_1:5
.= setsum Y01 by RLVECT_1:4 ;
(seq . n) - (seq . m) = ((seq . n) - (seq . m)) + (0. X) by RLVECT_1:4
.= ((seq . n) - (seq . m)) + ((seq . k) - (seq . k)) by RLVECT_1:5
.= (seq . n) - ((seq . m) - ((seq . k) - (seq . k))) by RLVECT_1:29
.= (seq . n) - (((seq . m) - (seq . k)) + (seq . k)) by RLVECT_1:29
.= (seq . n) - ((seq . k) - ((seq . k) - (seq . m))) by RLVECT_1:33
.= (setsum Y01) + (0. X) by A63, A58, RLVECT_1:29 ;
then ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(0. X).|| by BHSP_1:30;
then A64: ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + 0 by BHSP_1:26;
||.(setsum Y01).|| < 1 / (k + 1) by A32, A43, A60, A61;
then ||.(setsum Y01).|| < e / 2 by A38, XXREAL_0:2;
then ||.((seq . n) - (seq . m)).|| < e / 2 by A64, XXREAL_0:2;
then ||.((seq . n) - (seq . m)).|| + 0 < (e / 2) + (e / 2) by A35, XREAL_1:8;
hence ||.((seq . n) - (seq . m)).|| < e ; :: thesis: verum
end;
case A65: Y0 <> Y2 ; :: thesis: ||.((seq . n) - (seq . m)).|| < e
ex Y02 being finite Subset of X st
( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )
proof
take Y02 = Y2 \ Y0; :: thesis: ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )
A66: Y2 \ Y0 c= Y2 by XBOOLE_1:36;
Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
.= Y2 by A45, XBOOLE_1:12 ;
hence ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A41, A65, A66, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum
end;
then consider Y02 being finite Subset of X such that
A67: ( not Y02 is empty & Y02 c= Y ) and
A68: Y02 misses Y0 and
A69: Y0 \/ Y02 = Y2 ;
||.(setsum Y02).|| < 1 / (k + 1) by A32, A43, A67, A68;
then A70: ||.(setsum Y02).|| < e / 2 by A38, XXREAL_0:2;
ex Y01 being finite Subset of X st
( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )
proof
take Y01 = Y1 \ Y0; :: thesis: ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )
A71: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A48, XBOOLE_1:12 ;
hence ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A46, A57, A71, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum
end;
then consider Y01 being finite Subset of X such that
A72: ( not Y01 is empty & Y01 c= Y ) and
A73: Y01 misses Y0 and
A74: Y0 \/ Y01 = Y1 ;
setsum Y1 = (setsum Y0) + (setsum Y01) by A1, A73, A74, Th2;
then A75: (seq . n) - (seq . k) = (setsum Y01) + ((seq . k) + (- (seq . k))) by A44, A47, RLVECT_1:def 3
.= (setsum Y01) + (0. X) by RLVECT_1:5
.= setsum Y01 by RLVECT_1:4 ;
setsum Y2 = (setsum Y0) + (setsum Y02) by A1, A68, A69, Th2;
then A76: (seq . m) - (seq . k) = (setsum Y02) + ((seq . k) + (- (seq . k))) by A44, A42, RLVECT_1:def 3
.= (setsum Y02) + (0. X) by RLVECT_1:5
.= setsum Y02 by RLVECT_1:4 ;
(seq . n) - (seq . m) = ((seq . n) - (seq . m)) + (0. X) by RLVECT_1:4
.= ((seq . n) - (seq . m)) + ((seq . k) - (seq . k)) by RLVECT_1:5
.= (seq . n) - ((seq . m) - ((seq . k) - (seq . k))) by RLVECT_1:29
.= (seq . n) - (((seq . m) - (seq . k)) + (seq . k)) by RLVECT_1:29
.= (seq . n) - ((seq . k) - ((seq . k) - (seq . m))) by RLVECT_1:33
.= ((seq . n) - (seq . k)) + ((seq . k) + (- (seq . m))) by RLVECT_1:29
.= (setsum Y01) + (- (setsum Y02)) by A75, A76, RLVECT_1:33 ;
then ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(- (setsum Y02)).|| by BHSP_1:30;
then A77: ||.((seq . n) - (seq . m)).|| <= ||.(setsum Y01).|| + ||.(setsum Y02).|| by BHSP_1:31;
||.(setsum Y01).|| < 1 / (k + 1) by A32, A43, A72, A73;
then ||.(setsum Y01).|| < e / 2 by A38, XXREAL_0:2;
then ||.(setsum Y01).|| + ||.(setsum Y02).|| < (e / 2) + (e / 2) by A70, XREAL_1:8;
hence ||.((seq . n) - (seq . m)).|| < e by A77, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence ||.((seq . n) - (seq . m)).|| < e ; :: thesis: verum
end;
end;
end;
hence ||.((seq . n) - (seq . m)).|| < e ; :: thesis: verum
end;
hence ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < e ; :: thesis: verum
end;
then seq is Cauchy by BHSP_3:2;
then seq is convergent by BHSP_3:def 4;
then consider x being Point of X such that
A78: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq . n) - x).|| < r by BHSP_2:9;
now
let e be Real; :: thesis: ( e > 0 implies ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e ) ) )
assume A79: e > 0 ; :: thesis: ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e ) )
A80: e / 2 > 0 / 2 by A79, XREAL_1:74;
then consider m being Element of NAT such that
A81: for n being Element of NAT st n >= m holds
||.((seq . n) - x).|| < e / 2 by A78;
ex i being Element of NAT st
( 1 / (i + 1) < e / 2 & i >= m )
proof
set p = e / 2;
consider k1 being Element of NAT such that
A82: (e / 2) " < k1 by SEQ_4:3;
take i = k1 + m; :: thesis: ( 1 / (i + 1) < e / 2 & i >= m )
k1 <= k1 + m by NAT_1:11;
then (e / 2) " < i by A82, XXREAL_0:2;
then ((e / 2) ") + 0 < i + 1 by XREAL_1:8;
then 1 / (i + 1) < 1 / ((e / 2) ") by A80, XREAL_1:76;
then 1 / (i + 1) < 1 * (((e / 2) ") ") by XCMPLX_0:def 9;
hence ( 1 / (i + 1) < e / 2 & i >= m ) by NAT_1:11; :: thesis: verum
end;
then consider i being Element of NAT such that
A83: 1 / (i + 1) < e / 2 and
A84: i >= m ;
consider Y0 being finite Subset of X such that
A85: not Y0 is empty and
A86: A . i = Y0 and
A87: seq . i = setsum Y0 by A34;
A88: ||.((setsum Y0) - x).|| < e / 2 by A81, A84, A87;
now
let Y1 be finite Subset of X; :: thesis: ( Y0 c= Y1 & Y1 c= Y implies ||.(x - (setsum Y1)).|| < e )
assume that
A89: Y0 c= Y1 and
A90: Y1 c= Y ; :: thesis: ||.(x - (setsum Y1)).|| < e
now
per cases ( Y0 = Y1 or Y0 <> Y1 ) ;
case Y0 = Y1 ; :: thesis: ||.(x - (setsum Y1)).|| < e
then ||.(x - (setsum Y1)).|| = ||.(- (x - (setsum Y0))).|| by BHSP_1:31
.= ||.((setsum Y0) - x).|| by RLVECT_1:33 ;
then ||.(x - (setsum Y1)).|| < e / 2 by A81, A84, A87;
then ||.(x - (setsum Y1)).|| + 0 < (e / 2) + (e / 2) by A79, XREAL_1:8;
hence ||.(x - (setsum Y1)).|| < e ; :: thesis: verum
end;
case A91: Y0 <> Y1 ; :: thesis: ||.(x - (setsum Y1)).|| < e
ex Y2 being finite Subset of X st
( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 )
proof
take Y2 = Y1 \ Y0; :: thesis: ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 )
A92: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A89, XBOOLE_1:12 ;
hence ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 ) by A90, A91, A92, XBOOLE_1:1, XBOOLE_1:79; :: thesis: verum
end;
then consider Y2 being finite Subset of X such that
A93: ( not Y2 is empty & Y2 c= Y ) and
A94: Y0 misses Y2 and
A95: Y0 \/ Y2 = Y1 ;
(setsum Y1) - x = ((setsum Y0) + (setsum Y2)) - x by A1, A94, A95, Th2
.= ((setsum Y0) - x) + (setsum Y2) by RLVECT_1:def 3 ;
then ||.((setsum Y1) - x).|| <= ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| by BHSP_1:30;
then ||.(- ((setsum Y1) - x)).|| <= ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| by BHSP_1:31;
then A96: ||.(x + (- (setsum Y1))).|| <= ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| by RLVECT_1:33;
||.(setsum Y2).|| < 1 / (i + 1) by A32, A86, A93, A94;
then ||.(setsum Y2).|| < e / 2 by A83, XXREAL_0:2;
then ||.((setsum Y0) - x).|| + ||.(setsum Y2).|| < (e / 2) + (e / 2) by A88, XREAL_1:8;
hence ||.(x - (setsum Y1)).|| < e by A96, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence ||.(x - (setsum Y1)).|| < e ; :: thesis: verum
end;
hence ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e ) ) by A85, A86; :: thesis: verum
end;
hence Y is summable_set by Def2; :: thesis: verum
end;
now
assume Y is summable_set ; :: thesis: for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) )
then consider x being Point of X such that
A97: for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e ) ) by Def2;
now
let e be Real; :: thesis: ( e > 0 implies ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) )
assume e > 0 ; :: thesis: ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) )
then consider Y0 being finite Subset of X such that
A98: not Y0 is empty and
A99: Y0 c= Y and
A100: for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
||.(x - (setsum Y1)).|| < e / 2 by A97, XREAL_1:139;
reconsider Y0 = Y0 as non empty finite Subset of X by A98;
now
let Y1 be finite Subset of X; :: thesis: ( not Y1 is empty & Y1 c= Y & Y0 misses Y1 implies ||.(setsum Y1).|| < e )
assume that
not Y1 is empty and
A101: Y1 c= Y and
A102: Y0 misses Y1 ; :: thesis: ||.(setsum Y1).|| < e
set Z = Y0 \/ Y1;
Y0 c= Y0 \/ Y1 by XBOOLE_1:7;
then ||.(x - (setsum (Y0 \/ Y1))).|| < e / 2 by A99, A100, A101, XBOOLE_1:8;
then A103: ||.(x - (setsum (Y0 \/ Y1))).|| + ||.(x - (setsum Y0)).|| < (e / 2) + (e / 2) by A99, A100, XREAL_1:8;
||.((x - (setsum (Y0 \/ Y1))) - (x - (setsum Y0))).|| <= ||.(x - (setsum (Y0 \/ Y1))).|| + ||.(- (x - (setsum Y0))).|| by BHSP_1:30;
then A104: ||.((x - (setsum (Y0 \/ Y1))) - (x - (setsum Y0))).|| <= ||.(x - (setsum (Y0 \/ Y1))).|| + ||.(x - (setsum Y0)).|| by BHSP_1:31;
(setsum (Y0 \/ Y1)) - (setsum Y0) = ((setsum Y1) + (setsum Y0)) - (setsum Y0) by A1, A102, Th2
.= (setsum Y1) + ((setsum Y0) + (- (setsum Y0))) by RLVECT_1:def 3
.= (setsum Y1) + (0. X) by RLVECT_1:5
.= setsum Y1 by RLVECT_1:4 ;
then ||.(setsum Y1).|| = ||.(- ((setsum (Y0 \/ Y1)) - (setsum Y0))).|| by BHSP_1:31
.= ||.((setsum Y0) - (setsum (Y0 \/ Y1))).|| by RLVECT_1:33
.= ||.((0. X) + ((setsum Y0) - (setsum (Y0 \/ Y1)))).|| by RLVECT_1:4
.= ||.((x - x) + ((setsum Y0) - (setsum (Y0 \/ Y1)))).|| by RLVECT_1:5
.= ||.(x - (x - ((setsum Y0) - (setsum (Y0 \/ Y1))))).|| by RLVECT_1:29
.= ||.(x - ((x - (setsum Y0)) + (setsum (Y0 \/ Y1)))).|| by RLVECT_1:29
.= ||.((x - (setsum (Y0 \/ Y1))) - (x - (setsum Y0))).|| by RLVECT_1:27 ;
hence ||.(setsum Y1).|| < e by A104, A103, XXREAL_0:2; :: thesis: verum
end;
hence ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) by A99; :: thesis: verum
end;
hence for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) ; :: thesis: verum
end;
hence ( Y is summable_set iff for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) ) by A2; :: thesis: verum