:: On Some Properties of Real {H}ilbert Space, {I} :: by Hiroshi Yamazaki , Yasumasa Suzuki , Takao Inou\'e and Yasunari Shidama :: :: Received February 25, 2003 :: Copyright (c) 2003 Association of Mizar Users environ vocabularies BOOLE, PRE_TOPC, NORMSP_1, SEQ_2, RLVECT_1, FUNCT_1, ARYTM_1, FINSET_1, BHSP_1, BHSP_3, ABSVALUE, RELAT_1, ARYTM_3, BINOP_1, FUNCT_2, VECTSP_1, HAHNBAN, FINSEQ_1, SETWISEO, CARD_1, FINSOP_1, BHSP_5, BHSP_6, SEMI_AF1, JORDAN2C, ARYTM, ALGSTR_0; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, RELSET_1, FINSET_1, BINOP_2, PARTFUN1, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, BHSP_1, BHSP_2, BHSP_3, BINOP_1, SETWISEO, HAHNBAN, FINSEQ_1, FINSOP_1, BHSP_5; constructors PARTFUN1, BINOP_1, SETWISEO, REAL_1, NAT_1, NAT_D, BINOP_2, FINSOP_1, BHSP_2, BHSP_3, HAHNBAN, BHSP_5, SUPINF_1; registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, BINOP_2, MEMBERED, STRUCT_0; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; definitions RLVECT_1, ALGSTR_0; theorems XBOOLE_0, XBOOLE_1, REAL_2, TARSKI, REAL_1, ABSVALUE, FINSEQ_1, INT_1, FINSEQ_4, FUNCT_1, NAT_1, FUNCT_2, RLVECT_1, VECTSP_1, SEQ_4, BHSP_1, BHSP_2, BHSP_3, BHSP_5, HAHNBAN, FINSOP_1, CARD_2, FINSEQ_3, XCMPLX_0, XCMPLX_1, BINOP_2, XREAL_1, COMPLEX1, XXREAL_0; schemes NAT_1, FUNCT_2; begin :: Preliminaries reserve X for RealUnitarySpace; reserve x for Point of X; reserve i, n for Element of NAT; definition let X such that A1: the addF of X is commutative associative & the addF of X has_a_unity; let Y be finite Subset of X; func setsum Y -> Element of X means :Def1: ex p being FinSequence of the carrier of X st p is one-to-one & rng p = Y & it = (the addF of X) "**" p; existence proof consider p being FinSequence such that A2: rng p = Y and A3: p is one-to-one by FINSEQ_4:73; reconsider q = p as FinSequence of the carrier of X by A2,FINSEQ_1:def 4; ex p being FinSequence of the carrier of X st p is one-to-one & rng p = Y & (the addF of X) "**" q = (the addF of X) "**" p by A2,A3; hence thesis; end; uniqueness proof let X1, X2 be Element of X such that A4: ex p1 being FinSequence of the carrier of X st p1 is one-to-one & rng p1 = Y & X1 = (the addF of X) "**" p1 and A5: ex p2 being FinSequence of the carrier of X st p2 is one-to-one & rng p2 = Y & X2 = (the addF of X) "**" p2; consider p1 being FinSequence of the carrier of X such that A6: p1 is one-to-one and A7: rng p1 = Y and A8: X1 = (the addF of X) "**" p1 by A4; consider p2 being FinSequence of the carrier of X such that A9: p2 is one-to-one and A10: rng p2 = Y and A11: X2 = (the addF of X) "**" p2 by A5; dom p1 = dom p2 & ex P being Permutation of dom p1 st p2 = p1*P & dom P = dom p1 & rng P = dom p1 by A6,A7,A9,A10,BHSP_5:1; then consider P being Permutation of dom p1 such that A12: p2 = p1 * P; thus thesis by A1,A8,A11,A12,FINSOP_1:8; end; end; theorem Th1: for X st the addF of X is commutative associative & the addF of X has_a_unity for Y be finite Subset of X for I be Function of the carrier of X,the carrier of X st Y c= dom I & for x be set st x in dom I holds I.x = x holds setsum(Y) = setopfunc(Y, the carrier of X, the carrier of X, I, the addF of X) proof let X such that A1: the addF of X is commutative associative & the addF of X has_a_unity; let Y be finite Subset of X; let I be Function of the carrier of X,the carrier of X such that A2: Y c= dom I & for x be set st x in dom I holds I.x = x; consider p being FinSequence of the carrier of X such that A3: p is one-to-one & rng p = Y & setsum(Y) = (the addF of X) "**" p by A1,Def1; A4: dom Func_Seq(I,p)=dom p proof now let xd be set; A5: xd in dom(Func_Seq(I,p)) iff xd in dom(I*p) by BHSP_5:def 4; xd in dom p implies p.xd in rng(p) by FUNCT_1:12; hence xd in dom(Func_Seq(I,p)) iff xd in dom p by A2,A3,A5,FUNCT_1:21; end; hence thesis by TARSKI:2; end; now let s be set; assume A6: s in dom Func_Seq(I,p); then reconsider i = s as Element of NAT; A7: p.i in rng(p) by A4,A6,FUNCT_1:12; Func_Seq(I,p).s = (I*p).i by BHSP_5:def 4 .= I.(p.i) by A4,A6,FUNCT_1:23 .= p.i by A2,A3,A7; hence Func_Seq(I,p).s = p.s; end; then Func_Seq(I,p) =p by A4,FUNCT_1:9; hence thesis by A1,A2,A3,BHSP_5:def 5; end; theorem Th2: for X st the addF of X is commutative associative & the addF of X has_a_unity for Y1, Y2 be finite Subset of X st Y1 misses Y2 for Z be finite Subset of X st Z = Y1 \/ Y2 holds setsum(Z) = setsum(Y1) + setsum(Y2) proof let X such that A1: the addF of X is commutative associative & the addF of X has_a_unity; let Y1, Y2 be finite Subset of X such that A2: Y1 misses Y2; let Z be finite Subset of X such that A3: Z = Y1 \/ Y2; reconsider I = id the carrier of X as Function of the carrier of X, the carrier of X; A4: for x be set st x in the carrier of X holds I.x = x by FUNCT_1:35; A5: dom I = the carrier of X by FUNCT_2:def 1; then A6: setsum(Y1) = setopfunc(Y1,the carrier of X,the carrier of X,I,the addF of X) by A1,A4,Th1; A7: setsum(Y2) = setopfunc(Y2,the carrier of X,the carrier of X,I,the addF of X) by A1,A4,A5,Th1; setopfunc(Z,the carrier of X,the carrier of X,I,the addF of X) =setopfunc(Y1,the carrier of X,the carrier of X,I,the addF of X) + setopfunc(Y2,the carrier of X,the carrier of X,I,the addF of X) by A1,A2,A3 ,A5,BHSP_5:14; hence thesis by A1,A4,A5,A6,A7,Th1; end; begin :: Summability definition let X; let Y be Subset of X; attr Y is summable_set means :Def2: ex x st for e be Real st e > 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.x-setsum(Y1).|| < e; end; definition let X; let Y be Subset of X; assume A1: Y is summable_set; func sum Y -> Point of X means for e be Real st e > 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.it-setsum(Y1).|| < e; existence by A1,Def2; uniqueness proof let y1, y2 be Point of X such that A2: for e1 be Real st e1 > 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.y1-setsum(Y1).|| < e1 and A3: for e2 be Real st e2 > 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.y2-setsum(Y1).|| < e2; A4: now let e3 be Real such that A5: e3 >0; set e4 = e3/2; A6: e4 is Real & e4 >0 by A5,REAL_2:127; A7: e3/2 + e3/2 = e3; consider Y01 be finite Subset of X such that A8: Y01 is non empty & Y01 c= Y & for Y1 be finite Subset of X st Y01 c= Y1 & Y1 c= Y holds ||.y1-setsum(Y1).|| < e4 by A2,A6; consider Y02 be finite Subset of X such that A9: Y02 is non empty & Y02 c= Y & for Y1 be finite Subset of X st Y02 c= Y1 & Y1 c= Y holds ||.y2-setsum(Y1).|| < e4 by A3,A6; set Y00 = Y01 \/ Y02; A10: Y00 c= Y by A8,A9,XBOOLE_1:8; A11: Y00 is finite Subset of X & Y01 c= Y00 by XBOOLE_1:7; ||.y2-setsum(Y00).|| < e4 by A9,A10,XBOOLE_1:7; then ||.-(y2-setsum(Y00)).|| < e4 by BHSP_1:37; then ||.y1-setsum(Y00).|| + ||.-(y2-setsum(Y00)).|| < e3 by A7,A8,A10,A11,XREAL_1:10; then (||.y1-setsum(Y00) + -(y2-setsum(Y00)).||) + (||.y1-setsum(Y00).|| + ||.-(y2-setsum(Y00)).||) < (||.y1-setsum(Y00).|| + ||.-(y2-setsum(Y00)).||) + e3 by BHSP_1:36,XREAL_1:10; then A12: ||.y1-setsum(Y00) + -(y2-setsum(Y00)).|| + (||.y1-setsum(Y00).|| + ||.-(y2-setsum(Y00)).||) + - (||.y1-setsum(Y00).|| + ||.-(y2-setsum(Y00)).||) < e3 + (||.y1-setsum(Y00).|| + ||.-(y2-setsum(Y00)).||) + - (||.y1-setsum(Y00).|| + ||.-(y2-setsum(Y00)).||) by XREAL_1:10; ||.y1 - y2.|| = ||.(y1 - y2) + 0.X.|| by RLVECT_1:def 7 .= ||.(y1 - y2) + (setsum(Y00) - setsum(Y00)).|| by RLVECT_1:16 .= ||.((y1 - y2) + setsum(Y00)) - setsum(Y00).|| by RLVECT_1:def 6 .= ||.(y1 - (y2 - setsum(Y00))) - setsum(Y00).|| by RLVECT_1:43 .= ||.y1 - (setsum(Y00) + (y2 - setsum(Y00))).|| by RLVECT_1:41 .= ||.(y1 - setsum(Y00)) - (y2 - setsum(Y00)).|| by RLVECT_1:41 .= ||.(y1 - setsum(Y00)) + - (y2 - setsum(Y00)).||; hence ||.y1 - y2.|| < e3 by A12; end; y1 = y2 proof assume y1 <> y2; then y1 - y2 <> 0.X by VECTSP_1:66; then A13: ||.y1 - y2.|| <> 0 by BHSP_1:32; 0 <= ||.y1 - y2.|| by BHSP_1:34; hence contradiction by A4,A13; end; hence thesis; end; end; definition let X; let L be linear-Functional of X; attr L is Bounded means :Def4: ex K be Real st K > 0 & for x holds abs(L.x) <= K * ||.x.||; end; definition let X; let Y be Subset of X; attr Y is weakly_summable_set means :Def5: ex x st for L be linear-Functional of X st L is Bounded for e be Real st e > 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs(L.(x-setsum(Y1))) < e; end; definition let X; let Y be Subset of X; let L be Functional of X; pred Y is_summable_set_by L means :Def6: ex r be Real st for e be Real st e > 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs(r-setopfunc(Y1,the carrier of X,REAL, L, addreal)) < e; end; definition let X; let Y be Subset of X; let L be Functional of X; assume A1: Y is_summable_set_by L; func sum_byfunc(Y,L) -> Real means for e be Real st e > 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs(it-setopfunc(Y1,the carrier of X,REAL, L, addreal)) < e; existence by A1,Def6; uniqueness proof let r1, r2 be Real such that A2: for e1 be Real st e1 > 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs(r1-setopfunc(Y1,the carrier of X,REAL, L, addreal)) < e1 and A3: for e2 be Real st e2 > 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs(r2-setopfunc(Y1,the carrier of X,REAL, L, addreal)) < e2; A4: now let e3 be real number such that A5: e3 >0; set e4 = e3/2; A6: e4 is Real & e4 > 0 by A5,REAL_2:127; A7: e3/2 + e3/2 = e3; consider Y01 be finite Subset of X such that A8: Y01 is non empty & Y01 c= Y & for Y1 be finite Subset of X st Y01 c= Y1 & Y1 c= Y holds abs(r1-setopfunc(Y1,the carrier of X,REAL, L, addreal)) < e4 by A2,A6; consider Y02 be finite Subset of X such that A9: Y02 is non empty & Y02 c= Y & for Y1 be finite Subset of X st Y02 c= Y1 & Y1 c= Y holds abs(r2-setopfunc(Y1,the carrier of X,REAL, L, addreal)) < e4 by A3,A6; set Y00 = Y01 \/ Y02; A10: Y00 c= Y by A8,A9,XBOOLE_1:8; A11: Y00 is finite Subset of X & Y01 c= Y00 by XBOOLE_1:7; A12: abs(r2-setopfunc(Y00,the carrier of X,REAL, L, addreal)) < e4 by A9,A10,XBOOLE_1:7; A13: abs((r1-setopfunc(Y00,the carrier of X,REAL, L, addreal)) - (r2-setopfunc(Y00,the carrier of X,REAL, L, addreal))) <= abs(r1-setopfunc(Y00,the carrier of X,REAL, L, addreal)) + abs(r2-setopfunc(Y00,the carrier of X,REAL, L, addreal)) by COMPLEX1:143; abs(r1-setopfunc(Y00,the carrier of X,REAL, L, addreal)) + abs(r2-setopfunc(Y00,the carrier of X,REAL, L, addreal)) < e3 by A7,A8,A10,A11,A12,XREAL_1:10; hence abs(r1-r2) < e3 by A13,XXREAL_0:2; end; r1 = r2 proof assume A14: r1 <> r2; A15: abs(r1-r2) <> 0 proof assume abs(r1-r2) = 0; then r1-r2 = 0 by ABSVALUE:7; hence contradiction by A14; end; 0 <= abs(r1-r2) by COMPLEX1:132; hence contradiction by A4,A15; end; hence thesis; end; end; theorem Th3: for Y be Subset of X st Y is summable_set holds Y is weakly_summable_set proof let Y be Subset of X; assume Y is summable_set; then consider x such that A1: for e be Real st 0 < e ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.x - setsum(Y1).|| < e by Def2; now let L be linear-Functional of X such that A2: L is Bounded; consider K be Real such that A3: 0 < K & for x holds abs(L.x) <= K * ||.x.|| by A2,Def4; now let e1 be Real such that A4: 0 < e1; set e = e1/K; A5: 0 < e by A3,A4,REAL_2:127; A6: e * K = e1 by A3,XCMPLX_1:88; consider Y0 be finite Subset of X such that A7: Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c=Y holds ||.x - setsum(Y1).|| < e by A1,A5; now let Y1 be finite Subset of X such that A8: Y0 c= Y1 & Y1 c=Y; K * ||.x - setsum(Y1).|| < e1 by A3,A6,XREAL_1:70,A7,A8; then abs (L.(x-setsum(Y1))) + K*||.(x-setsum(Y1)).|| < K*||.(x-setsum(Y1)).|| + e1 by A3,XREAL_1:10; then abs (L.(x-setsum(Y1))) + K*||.(x-setsum(Y1)).|| - K*||.(x-setsum(Y1)).|| < K*||.(x-setsum(Y1)).|| + e1 - K*||.(x-setsum(Y1)).|| by REAL_1:92; hence abs (L.(x-setsum(Y1))) < e1; end; hence ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c=Y holds abs (L.(x-setsum(Y1))) < e1 by A7; end; hence for e1 be Real st 0 < e1 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c=Y holds abs (L.(x-setsum(Y1))) < e1; end; hence thesis by Def5; end; theorem Th4: for L be linear-Functional of X for p be FinSequence of the carrier of X st len p >=1 for q be FinSequence of REAL st dom p = dom q & (for i st i in dom q holds q.i = L.(p.i) ) holds L.((the addF of X) "**" p) = addreal "**" q proof let L be linear-Functional of X; let p be FinSequence of the carrier of X such that A1: len p >= 1; let q be FinSequence of REAL such that A2: dom p = dom q & (for i st i in dom q holds q.i = L.(p.i)); consider f be Function of NAT,the carrier of X such that A3: f.1 = p.1 and A4: (for n be Element of NAT st 0 <> n & n < len p holds f.(n + 1) = (the addF of X).(f.n,p.(n + 1))) and A5: (the addF of X) "**" p = f.(len p) by A1,FINSOP_1:2; Seg (len q) = dom p by A2,FINSEQ_1:def 3 .= Seg (len p) by FINSEQ_1:def 3; then A6: len q = len p by FINSEQ_1:8; then consider g be Function of NAT, REAL such that A7: g.1 = q.1 and A8: (for n be Element of NAT st 0 <> n & n < len q holds g.(n + 1) = addreal.(g.n,q.(n + 1))) and A9: addreal "**" q = g.(len q) by A1,FINSOP_1:2; defpred P[Element of NAT] means 1 <= $1 & $1 <= len q implies g.$1 = L.(f.$1); for n holds P[n] proof A10: P[0]; A11: now let n; assume A12: P[n]; now assume A13: 1 <=n+1 & n+1 <= len q; A14: n <= n+1 by NAT_1:11; per cases; suppose A15: n=0; 1 in dom p by A1,FINSEQ_3:27; hence g.(n+1) = L.(f.(n+1)) by A2,A3,A7,A15; end; suppose A16: n<>0; then 0 < n; then A17: 0+1 <= n by INT_1:20; A18: n+1-1 < len q-0 by A13,REAL_1:92; A19: n+1 in dom q by A13,FINSEQ_3:27; reconsider z=f.n as Element of X; p.(n+1) in rng p by A2,A19,FUNCT_1:12; then reconsider y=p.(n+1) as Element of X; reconsider z1=z as VECTOR of X; reconsider y1=y as VECTOR of X; set Lz=L.z1, Ly=L.y1; thus g.(n+1) = addreal.(g.n,q.(n + 1)) by A8,A16,A18 .= addreal.(L.(f.n), L.y) by A2,A12,A13,A14,A17,A19,XXREAL_0:2 .= Lz + Ly by BINOP_2:def 9 .= L .(z1+y1) by HAHNBAN:def 4 .= L.(f.(n + 1)) by A4,A6,A16,A18; end; end; hence P[n+1]; end; thus thesis from NAT_1:sch 1(A10,A11); end; hence thesis by A1,A5,A6,A9; end; theorem Th5: for X st the addF of X is commutative associative & the addF of X has_a_unity for S be finite Subset of X st S is non empty for L be linear-Functional of X holds L.(setsum(S)) = setopfunc(S,the carrier of X,REAL, L, addreal) proof let X such that A1: the addF of X is commutative associative & the addF of X has_a_unity; let S be finite Subset of X such that A2: S is non empty; let L be linear-Functional of X; A3: dom L = the carrier of X by FUNCT_2:def 1; consider p be FinSequence of the carrier of X such that A4: p is one-to-one & rng p = S & setsum(S) = (the addF of X) "**" p by A1,Def1; reconsider q1 = Func_Seq(L,p) as FinSequence of REAL; A5: dom Func_Seq(L,p)=dom p proof now let xd be set; A6: xd in dom(Func_Seq(L,p)) iff xd in dom(L*p) by BHSP_5:def 4; xd in dom p implies p.xd in rng(p) by FUNCT_1:12; hence xd in dom(Func_Seq(L,p)) iff xd in dom p by A3,A6,FUNCT_1:21; end; hence thesis by TARSKI:2; end; A7: for i st i in dom p holds q1.i = L.(p.i) proof let i such that A8: i in dom p; q1.i = (L*p).i by BHSP_5:def 4 .= L.(p.i) by A8,FUNCT_1:23; hence thesis; end; len p >=1 proof card S <> 0 by A2,CARD_2:59; then 0 < card S; then 0+1 <= card S by INT_1:20; hence thesis by A4,FINSEQ_4:77; end; then L.((the addF of X) "**" p) = addreal "**" q1 by A5,A7,Th4; hence thesis by A3,A4,BHSP_5:def 5; end; theorem Th6: for X st the addF of X is commutative associative & the addF of X has_a_unity for Y be Subset of X holds Y is weakly_summable_set implies ex x st for L be linear-Functional of X st L is Bounded for e be Real st e > 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs((L.x)-(setopfunc(Y1,the carrier of X,REAL, L, addreal))) < e proof let X such that A1: the addF of X is commutative associative & the addF of X has_a_unity; let Y be Subset of X; assume Y is weakly_summable_set; then consider x such that A2: for L be linear-Functional of X st L is Bounded for e be Real st e > 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs(L.(x-setsum(Y1))) < e by Def5; take x; now let L be linear-Functional of X such that A3: L is Bounded; now let e be Real such that A4: e > 0; consider Y0 be finite Subset of X such that A5: Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs(L.(x-setsum(Y1))) < e by A2,A3,A4; take Y0; now let Y1 be finite Subset of X such that A6: Y0 c= Y1 & Y1 c= Y; set r = L.(x-setsum(Y1)); set x1 = x; set y1 = setsum(Y1); A7: r = L.x1 - L.y1 by HAHNBAN:32; Y1 <> {} by A5,A6; then L.y1=setopfunc(Y1,the carrier of X,REAL, L, addreal) by A1,Th5; hence abs((L.x)-(setopfunc(Y1,the carrier of X,REAL, L, addreal))) < e by A5,A6,A7; end; hence Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs((L.x)-(setopfunc(Y1,the carrier of X,REAL, L, addreal))) < e by A5; end; hence for e be Real st e > 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs((L.x)-(setopfunc(Y1,the carrier of X,REAL, L, addreal))) < e; end; hence thesis; end; theorem Th7: for X st the addF of X is commutative associative & the addF of X has_a_unity for Y be Subset of X st Y is weakly_summable_set for L be linear-Functional of X st L is Bounded holds Y is_summable_set_by L proof let X such that A1: the addF of X is commutative associative & the addF of X has_a_unity; let Y be Subset of X such that A2: Y is weakly_summable_set; let L be linear-Functional of X such that A3: L is Bounded; consider x such that A4: for L be linear-Functional of X st L is Bounded for e be Real st e > 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs((L.x)-(setopfunc(Y1,the carrier of X,REAL, L, addreal))) < e by A1,A2,Th6; for e be Real st e > 0 ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds abs((L.x)-(setopfunc(Y1,the carrier of X,REAL, L, addreal))) < e by A3,A4; hence thesis by Def6; end; theorem for X st the addF of X is commutative associative & the addF of X has_a_unity for Y be Subset of X st Y is summable_set for L be linear-Functional of X st L is Bounded holds Y is_summable_set_by L by Th3,Th7; theorem for Y be finite Subset of X st Y is non empty holds Y is summable_set proof let Y be finite Subset of X such that A1: Y is non empty; set x = setsum Y; now let e be Real such that A2: e >0; ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.x-setsum(Y1).|| < e proof take Y; now let Y1 be finite Subset of X such that A3: Y c= Y1 & Y1 c= Y; Y1 = Y by A3,XBOOLE_0:def 10; then x - setsum(Y1) = 0.X by RLVECT_1:28; hence ||.x-setsum(Y1).|| < e by A2,BHSP_1:32; end; hence thesis by A1; end; hence ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.x-setsum(Y1).|| < e; end; hence thesis by Def2; end; begin :: Necessary and sufficient condition for summability theorem for X st the addF of X is commutative associative & the addF of X has_a_unity & X is_Hilbert_space for Y be Subset of X holds Y is summable_set iff (for e be Real st e > 0 holds ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds ||.setsum(Y1).|| < e)) proof let X such that A1: the addF of X is commutative associative & the addF of X has_a_unity & X is_Hilbert_space; let Y be Subset of X; A2: now assume Y is summable_set; then consider x such that A3: for e be Real st e > 0 holds ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.x-setsum(Y1).|| < e by Def2; now let e be Real such that A4: e > 0; 0 < e/2 by A4,REAL_2:127; then consider Y0 be finite Subset of X such that A5: Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.x-setsum(Y1).|| < e/2 by A3; reconsider Y0 as finite non empty Subset of X by A5; now let Y1 be finite Subset of X such that A6: Y1 is non empty & Y1 c= Y & Y0 misses Y1; set Z = Y0 \/ Y1; setsum(Z) - setsum(Y0) = setsum(Y1) + setsum(Y0) - setsum(Y0) by A1,A6,Th2 .= setsum(Y1) + (setsum(Y0) +- setsum(Y0)) by RLVECT_1:def 6 .= setsum(Y1) + 0.X by RLVECT_1:16 .= setsum(Y1) by RLVECT_1:10; then A7: ||.setsum(Y1).|| = ||.-(setsum(Z) - setsum(Y0)).|| by BHSP_1:37 .= ||.setsum(Y0) - setsum(Z).|| by RLVECT_1:47 .= ||.0.X + (setsum(Y0) - setsum(Z)).|| by RLVECT_1:10 .= ||.(x - x) + (setsum(Y0) - setsum(Z)).|| by RLVECT_1:16 .= ||.x - (x - (setsum(Y0) - setsum(Z))).|| by RLVECT_1:43 .= ||.x - ((x - setsum(Y0)) + setsum(Z)).|| by RLVECT_1:43 .= ||.(x - setsum(Z)) - (x - setsum(Y0)).|| by RLVECT_1:41; ||.(x-setsum(Z))-(x-setsum(Y0)).|| <= ||.(x-setsum(Z)).|| + ||.-(x-setsum(Y0)).|| by BHSP_1:36; then A8: ||.(x-setsum(Z))-(x-setsum(Y0)).|| <= ||.(x-setsum(Z)).|| + ||.(x-setsum(Y0)).|| by BHSP_1:37; Y0 c= Z & Z c= Y by A5,A6,XBOOLE_1:7,8; then ||.x - setsum(Z).|| < e/2 by A5; then ||.(x - setsum(Z)).|| + ||.(x - setsum(Y0)).|| < e/2 + e/2 by A5,XREAL_1:10; hence ||.setsum(Y1).|| < e by A7,A8,XXREAL_0:2; end; hence ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds ||.setsum(Y1).|| < e by A5; end; hence for e be Real st e > 0 holds ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds ||.setsum(Y1).|| < e; end; :::: <= :::: now assume A9: for e be Real st e > 0 holds ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds ||.setsum(Y1).|| < e; defpred P[set,set] means ( $2 is finite Subset of X & $2 is non empty & $2 c= Y & for z be Real st z=$1 for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & $2 misses Y1 holds ||.setsum(Y1).|| < 1/(z+1)); A10: ex B being Function of NAT, bool Y st for x be set st x in NAT holds P[x,B.x] proof A11: now let x be set such that A12: x in NAT; reconsider xx= x as Element of NAT by A12; reconsider e = 1/(xx+1) as Real; 0/(xx + 1) < 1/(xx + 1) by REAL_1:73; then consider Y0 be finite Subset of X such that A13: Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds ||.setsum(Y1).|| < e by A9; for z be Real st z=x for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds ||.setsum(Y1).|| < 1/(z+1) by A13; hence ex y be set st y in bool Y & P[x,y] by A13; end; thus thesis from FUNCT_2:sch 1(A11); end; ex A be Function of NAT, bool Y st for i be Element of NAT holds A.i is finite Subset of X & A.i is non empty & A.i c= Y & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & A.i misses Y1 holds ||.setsum(Y1).|| < 1/(i+1)) & for j be Element of NAT st i <= j holds A.i c= A.j proof consider B being Function of NAT,bool Y such that A14: for x be set st x in NAT holds B.x is finite Subset of X & B.x is non empty & B.x c= Y & for z be Real st z=x for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & B.x misses Y1 holds ||.setsum(Y1).|| < 1/(z+1) by A10; deffunc G(Nat,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) = G(n,A.n) from NAT_1:sch 11; then consider A being Function such that A15: dom A = NAT & A.0 = B.0 & for n being Nat holds A.(n+1) = B.(n+1) \/ A.n; defpred R[Element of NAT] means A.$1 is finite Subset of X & A.$1 is non empty & A.$1 c= Y & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & A.$1 misses Y1 holds ||.setsum(Y1).|| < 1/($1+1)) & for j be Element of NAT st $1 <= j holds A.$1 c= A.j; for j0 be Element of NAT st j0=0 holds for j be Element of NAT st j0 <= j holds A.j0 c= A.j proof let j0 be Element of NAT such that A16: j0 = 0; defpred P[Element of NAT] means (j0 <= $1 implies A.j0 c= A.$1); A17: P[0]; A18: now let j be Element of NAT such that A19: P[j]; A.(j+1) = (B.(j+1) \/ A.j) by A15; then A.j c= A.(j+1) by XBOOLE_1:7; hence P[j+1] by A16,A19,XBOOLE_1:1; end; thus for j be Element of NAT holds P[j] from NAT_1:sch 1(A17, A18); end; then A20: R[0] by A14,A15; A21: now let n be Element of NAT such that A22: R[n]; A23: A.(n+1) = B.(n+1) \/ A.n by A15; A24: B.(n+1) is finite Subset of X by A14; A26: for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & A.(n+1) misses Y1 holds ||.setsum(Y1).|| < 1/((n+1)+1) proof let Y1 be finite Subset of X such that A27: Y1 is non empty & Y1 c= Y & A.(n+1) misses Y1; A.(n+1) = B.(n+1) \/ A.n by A15; then B.(n+1) misses Y1 by A27,XBOOLE_1:7,63; hence ||.setsum(Y1).|| < 1/((n+1)+1) by A14,A27; end; defpred P[Element of NAT] means (n+1) <= $1 implies A.(n+1) c= A.$1; for j be Element of NAT holds P[j] proof A28: P[0]; A29: for j being Element of NAT st P[j] holds P[j+1] proof let j be Element of NAT such that A30: n+1 <= j implies A.(n+1) c= A.j and A31: n+1 <= j+1; per cases; suppose n = j; hence A.(n+1) c= A.(j+1); end; suppose A32: n <> j; n <= j by A31,XREAL_1:8; then A33: n < j by A32,REAL_1:def 5; A.(j+1) = (B.(j+1) \/ A.j) by A15; then A.j c= A.(j+1) by XBOOLE_1:7; hence A.(n+1) c= A.(j+1) by A30,A33,NAT_1:13,XBOOLE_1:1; end; end; thus thesis from NAT_1:sch 1(A28, A29); end; hence R[n+1] by A22,A23,A24,A26,XBOOLE_1:8; end; A34: for i be Element of NAT holds R[i] from NAT_1:sch 1(A20,A21); now let y be set such that A35: y in rng A; consider x be set such that A36: x in dom A & y = A.x by A35,FUNCT_1:def 5; reconsider i = x as Element of NAT by A15,A36; A.i c= Y by A34; hence y in bool Y by A36; end; then rng A c= bool Y by TARSKI:def 3; then A is Function of NAT, bool Y by A15,FUNCT_2:4; hence thesis by A34; end; then consider A be Function of NAT, bool Y such that A37: for i be Element of NAT holds A.i is finite Subset of X & A.i is non empty & A.i c= Y & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & A.i misses Y1 holds ||.setsum(Y1).|| < 1/(i+1)) & for j be Element of NAT st i <= j holds A.i c= A.j; defpred P[set,set] means ex Y1 be finite Subset of X st Y1 is non empty & A.$1 = Y1 & $2=setsum(Y1); A38: for x be set st x in NAT ex y be set st y in the carrier of X & P[x,y] proof let x be set such that A39: x in NAT; reconsider i=x as Element of NAT by A39; A40: A.i is finite Subset of X & A.i is non empty & A.i c= Y & (for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & A.x misses Y1 holds ||.setsum(Y1).|| < 1/(i+1)) & for j be Element of NAT st i <= j holds A.i c= A.j by A37; then reconsider Y1 = A.x as finite Subset of X; reconsider y = setsum(Y1) as set; y in the carrier of X & ex Y1 be finite Subset of X st Y1 is non empty set & A.x = Y1 & y = setsum(Y1) by A40; hence thesis; end; ex F being Function of NAT, the carrier of X st for x be set st x in NAT holds P[x,F.x] from FUNCT_2:sch 1(A38); then consider F being Function of NAT, the carrier of X such that A41: for x be set st x in NAT holds ex Y1 be finite Subset of X st Y1 is non empty & A.x = Y1 & F.x = setsum(Y1); reconsider seq = F as sequence of X; A42: seq is_Cauchy_sequence proof now let e be Real such that A43: e > 0; A44: e/2 > 0/2 by A43,REAL_1:73; ex k be Element of NAT st 1/(k+1) < e/2 proof set p = e/2; A45: 0= k & m >= k; consider Y0 be finite Subset of X such that A49: Y0 is non empty & A.k = Y0 & seq.k = setsum(Y0) by A41; consider Y1 be finite Subset of X such that A50: Y1 is non empty & A.n = Y1 & seq.n = setsum(Y1) by A41; consider Y2 be finite Subset of X such that A51: Y2 is non empty & A.m = Y2 & seq.m = setsum(Y2) by A41; A52: Y0 c= Y1 by A37,A48,A49,A50; A53: Y0 c= Y2 by A37,A48,A49,A51; now per cases; case A54: Y0 = Y1; now per cases; case Y0 = Y2; then (seq.n) - (seq.m) = 0.X by A50,A51,A54,RLVECT_1:16; hence ||.(seq.n) - (seq.m).|| < e by A43,BHSP_1:32; end; case A55: Y0 <> Y2; ex Y02 be finite Subset of X st Y02 is non empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 proof take Y02 = Y2 \ Y0; A56: Y2 \ Y0 c= Y2 by XBOOLE_1:36; Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39 .= Y2 by A53,XBOOLE_1:12; hence thesis by A51,A55,A56,XBOOLE_1:1,79; end; then consider Y02 be finite Subset of X such that A57: Y02 is non empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2; A58: setsum(Y2) = setsum(Y0) + setsum(Y02) by A1,A57,Th2; ||.setsum(Y02).|| < 1/(k+1) by A37,A49,A57; then A59: ||.setsum(Y02).|| < e/2 by A47,XXREAL_0:2; A60: e*(1/2) < e*1 by A43,XREAL_1:70; ||.(seq.n) - (seq.m).|| = ||.(setsum(Y0) - setsum(Y0)) - setsum(Y02).|| by A50,A51,A54,A58,RLVECT_1:41 .= ||.0.X - setsum(Y02).|| by RLVECT_1:28 .= ||. - setsum(Y02).|| by RLVECT_1:27 .= ||.setsum(Y02).|| by BHSP_1:37; hence ||.(seq.n) - (seq.m).|| < e by A59,A60,XXREAL_0:2; end; end; hence ||.(seq.n) - (seq.m).|| < e; end; case A61: Y0 <> Y1; now per cases; case A62: Y0 = Y2; ex Y01 be finite Subset of X st Y01 is non empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 proof take Y01 = Y1 \ Y0; A63: Y1 \ Y0 c= Y1 by XBOOLE_1:36; Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39 .= Y1 by A52,XBOOLE_1:12; hence thesis by A50,A61,A63,XBOOLE_1:1,79; end; then consider Y01 be finite Subset of X such that A64: Y01 is non empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1; seq.n = seq.k + setsum(Y01) by A1,A49,A50,A64,Th2; then A65: seq.n - seq.k = seq.k + (setsum(Y01) +- seq.k) by RLVECT_1:def 6 .= seq.k - (seq.k - setsum(Y01)) by RLVECT_1:47 .= (setsum(Y0) - setsum(Y0)) + setsum(Y01) by A49,RLVECT_1:43 .= 0.X + setsum(Y01) by RLVECT_1:16 .= setsum(Y01) by RLVECT_1:10; A66: seq.k - seq.m = 0.X by A49,A51,A62,RLVECT_1:16; seq.n - seq.m = seq.n - seq.m + 0.X by RLVECT_1:10 .= seq.n - seq.m + (seq.k - seq.k) by RLVECT_1:16 .= seq.n - (seq.m - (seq.k - seq.k)) by RLVECT_1:43 .= seq.n - ((seq.m - seq.k) + seq.k) by RLVECT_1:43 .= seq.n - (seq.k - (seq.k - seq.m)) by RLVECT_1:47 .= setsum(Y01) + 0.X by A65,A66,RLVECT_1:43; then ||.(seq.n) - (seq.m).|| <= ||.setsum(Y01).|| + ||.0.X.|| by BHSP_1:36; then A67: ||.(seq.n) - (seq.m).|| <= ||.setsum( Y01).|| + 0 by BHSP_1:32; ||. setsum(Y01).|| < 1/(k+1) by A37,A49,A64; then ||. setsum(Y01).|| < e/2 by A47,XXREAL_0:2; then ||.(seq.n) - (seq.m).|| < e/2 by A67,XXREAL_0:2; then ||.(seq.n) - (seq.m).|| + 0 < e/2 + e/2 by A43,XREAL_1:10; hence ||.(seq.n) - (seq.m).|| < e; end; case A68: Y0<>Y2; ex Y01 be finite Subset of X st Y01 is non empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 proof take Y01 = Y1 \ Y0; A69: Y1 \ Y0 c= Y1 by XBOOLE_1:36; Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39 .= Y1 by A52,XBOOLE_1:12; hence thesis by A50,A61,A69,XBOOLE_1:1,79; end; then consider Y01 be finite Subset of X such that A70: Y01 is non empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1; ex Y02 be finite Subset of X st Y02 is non empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 proof take Y02 = Y2 \ Y0; A71: Y2 \ Y0 c= Y2 by XBOOLE_1:36; Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39 .= Y2 by A53,XBOOLE_1:12; hence thesis by A51,A68,A71,XBOOLE_1:1,79; end; then consider Y02 be finite Subset of X such that A72: Y02 is non empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2; ||. setsum(Y01).|| < 1/(k+1) by A37,A49,A70; then A73: ||. setsum(Y01).|| < e/2 by A47,XXREAL_0:2; ||.setsum(Y02).|| < 1/(k+1) by A37,A49,A72; then ||.setsum(Y02).|| < e/2 by A47,XXREAL_0:2; then A74: ||.setsum(Y01).|| + ||. setsum(Y02).|| < e/2 + e/2 by A73,XREAL_1:10; A75: setsum(Y1) = setsum(Y0) + setsum(Y01) by A1,A70,Th2; A76: setsum(Y2) = setsum(Y0) + setsum(Y02) by A1,A72,Th2; A77: seq.n - seq.k = setsum(Y01) + (seq.k +- seq.k) by A49,A50,A75,RLVECT_1:def 6 .= setsum(Y01) + 0.X by RLVECT_1:16 .= setsum(Y01) by RLVECT_1:10; A78: seq.m - seq.k = setsum(Y02) + (seq.k +- seq.k) by A49,A51,A76,RLVECT_1:def 6 .= setsum(Y02) + 0.X by RLVECT_1:16 .= setsum(Y02) by RLVECT_1:10; seq.n - seq.m = seq.n - seq.m + 0.X by RLVECT_1:10 .= seq.n - seq.m + (seq.k - seq.k) by RLVECT_1:16 .= seq.n - (seq.m - (seq.k - seq.k)) by RLVECT_1:43 .= seq.n - ((seq.m - seq.k) + seq.k) by RLVECT_1:43 .= seq.n - (seq.k - (seq.k - seq.m)) by RLVECT_1:47 .= (seq.n - seq.k) + (seq.k +- seq.m) by RLVECT_1:43 .= setsum(Y01) +- setsum(Y02) by A77,A78,RLVECT_1:47; then ||.(seq.n) - (seq.m).|| <= ||. setsum(Y01).|| + ||. - setsum(Y02).|| by BHSP_1:36; then ||.(seq.n) - (seq.m).|| <= ||. setsum(Y01).|| + ||.setsum(Y02).|| by BHSP_1:37; hence ||.(seq.n) - (seq.m).|| < e by A74,XXREAL_0:2; end; end; hence ||.(seq.n) - (seq.m).|| < e; end; end; hence ||.(seq.n) - (seq.m).|| < e; end; hence ex k be Element of NAT st for n, m be Element of NAT st (n >= k & m >= k) holds ||.(seq.n) - (seq.m).|| < e; end; hence seq is_Cauchy_sequence by BHSP_3:2; end; X is_complete_space by A1,BHSP_3:def 7; then seq is convergent by A42,BHSP_3:def 6; then consider x such that A79: for r be Real st r > 0 ex m be Element of NAT st for n be Element of NAT st n >= m holds ||.seq.n - x.|| < r by BHSP_2:9; now let e be Real such that A80: e >0; A81: e/2 > 0/2 by A80,REAL_1:73; then consider m be Element of NAT such that A82: for n be Element of NAT st n >= m holds ||. (seq.n)-x .|| < e/2 by A79; ex i be Element of NAT st 1/(i+1) < e/2 & i >= m proof set p = e/2; A83: 0= m; consider Y0 be finite Subset of X such that A86: Y0 is non empty & A.i = Y0 & seq.i=setsum(Y0) by A41; A87: ||.setsum(Y0) - x.|| < e/2 by A82,A85,A86; now let Y1 be finite Subset of X such that A88: Y0 c= Y1 & Y1 c= Y; now per cases; case Y0 = Y1; then ||.x - setsum(Y1).|| = ||.-(x - setsum(Y0)).|| by BHSP_1:37 .= ||.setsum(Y0) - x.|| by RLVECT_1:47; then ||.x - setsum(Y1).|| < e/2 by A82,A85,A86; then ||.x-setsum(Y1).|| + 0 < e/2 + e/2 by A80,XREAL_1:10; hence ||.x-setsum(Y1).|| < e; end; case A89: Y0 <> Y1; ex Y2 be finite Subset of X st Y2 is non empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 proof take Y2 = Y1 \ Y0; A90: Y1 \ Y0 c= Y1 by XBOOLE_1:36; Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39 .= Y1 by A88,XBOOLE_1:12; hence thesis by A88,A89,A90,XBOOLE_1:1,79; end; then consider Y2 be finite Subset of X such that A91: Y2 is non empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1; ||.setsum(Y2).|| < 1/(i+1) by A37,A86,A91; then A92: ||.setsum(Y2).|| < e/2 by A85,XXREAL_0:2; setsum(Y1) - x = setsum(Y0) + setsum(Y2) - x by A1,A91,Th2 .= setsum(Y0) - x + setsum(Y2) by RLVECT_1:def 6; then ||.setsum(Y1) - x.|| <= ||.setsum(Y0) - x.|| + ||.setsum(Y2).|| by BHSP_1:36; then ||.-(setsum(Y1) - x).|| <= ||.setsum(Y0) - x.|| + ||.setsum(Y2).|| by BHSP_1:37; then A93: ||.x +- setsum(Y1).|| <= ||.setsum(Y0) - x.|| + ||.setsum(Y2).|| by RLVECT_1:47; ||.setsum(Y0)-x.|| + ||.setsum(Y2).|| < e/2 + e/2 by A87,A92,XREAL_1:10; hence ||.x - setsum(Y1).|| < e by A93,XXREAL_0:2; end; end; hence ||.x-setsum(Y1).|| < e; end; hence ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.x-setsum(Y1).|| < e by A86; end; hence Y is summable_set by Def2; end; hence thesis by A2; end;