bhsp_6.miz



    begin

    reserve X for RealUnitarySpace;

    reserve x for Point of X;

    reserve i,n for Nat;

    definition

      let X;

      let Y be finite Subset of X;

      :: BHSP_6:def1

      func setsum Y -> Element of X means

      : Def1: ex p be 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 be FinSequence such that

         A2: ( rng p) = Y and

         A3: p is one-to-one by FINSEQ_4: 58;

        reconsider q = p as FinSequence of the carrier of X by A2, FINSEQ_1:def 4;

        ex p be 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 be 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 be FinSequence of the carrier of X st p2 is one-to-one & ( rng p2) = Y & X2 = (the addF of X "**" p2);

        consider p2 be FinSequence of the carrier of X such that

         A6: p2 is one-to-one & ( rng p2) = Y and

         A7: X2 = (the addF of X "**" p2) by A5;

        consider p1 be FinSequence of the carrier of X such that

         A8: p1 is one-to-one & ( rng p1) = Y and

         A9: X1 = (the addF of X "**" p1) by A4;

        ex P be Permutation of ( dom p1) st p2 = (p1 * P) & ( dom P) = ( dom p1) & ( rng P) = ( dom p1) by A8, A6, BHSP_5: 1;

        hence thesis by A1, A9, A7, FINSOP_1: 7;

      end;

    end

    theorem :: BHSP_6:1

    

     Th1: for X st the addF of X is commutative associative & the addF of X is having_a_unity holds for Y be finite Subset of X holds 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 is having_a_unity;

      let Y be finite Subset of X;

      consider p be FinSequence of the carrier of X such that

       A2: p is one-to-one and

       A3: ( rng p) = Y and

       A4: ( setsum Y) = (the addF of X "**" p) by A1, Def1;

      let I be Function of the carrier of X, the carrier of X such that

       A5: Y c= ( dom I) and

       A6: for x be set st x in ( dom I) holds (I . x) = x;

      now

        let xd be object;

        

         A7: xd in ( dom p) implies (p . xd) in ( rng p) by FUNCT_1: 3;

        xd in ( dom ( Func_Seq (I,p))) iff xd in ( dom (I * p)) by BHSP_5:def 4;

        hence xd in ( dom ( Func_Seq (I,p))) iff xd in ( dom p) by A5, A3, A7, FUNCT_1: 11;

      end;

      then

       A8: ( dom ( Func_Seq (I,p))) = ( dom p) by TARSKI: 2;

      now

        let s be object;

        assume

         A9: s in ( dom ( Func_Seq (I,p)));

        then

        reconsider i = s as Nat;

        

         A10: (p . i) in ( rng p) by A8, A9, FUNCT_1: 3;

        (( Func_Seq (I,p)) . s) = ((I * p) . i) by BHSP_5:def 4

        .= (I . (p . i)) by A8, A9, FUNCT_1: 13

        .= (p . i) by A5, A6, A3, A10;

        hence (( Func_Seq (I,p)) . s) = (p . s);

      end;

      then ( Func_Seq (I,p)) = p by A8, FUNCT_1: 2;

      hence thesis by A1, A2, A3, A4, BHSP_5:def 5;

    end;

    theorem :: BHSP_6:2

    

     Th2: for X st the addF of X is commutative associative & the addF of X is having_a_unity holds for Y1,Y2 be finite Subset of X st Y1 misses Y2 holds 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 is having_a_unity;

      reconsider I = ( id the carrier of X) as Function of the carrier of X, the carrier of X;

      let Y1,Y2 be finite Subset of X such that

       A2: Y1 misses Y2;

      

       A3: ( dom I) = the carrier of X by FUNCT_2:def 1;

      let Z be finite Subset of X;

      assume Z = (Y1 \/ Y2);

      then

       A4: ( 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, BHSP_5: 14;

      

       A5: for x be set st x in the carrier of X holds (I . x) = x by FUNCT_1: 18;

      then ( setsum Y1) = ( setopfunc (Y1,the carrier of X,the carrier of X,I,the addF of X)) & ( setsum Y2) = ( setopfunc (Y2,the carrier of X,the carrier of X,I,the addF of X)) by A1, A3, Th1;

      hence thesis by A1, A5, A3, A4, Th1;

    end;

    begin

    definition

      let X;

      let Y be Subset of X;

      :: BHSP_6:def2

      attr Y is summable_set means ex x st 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;

    end

    definition

      let X;

      let Y be Subset of X;

      assume

       A1: Y is summable_set;

      :: BHSP_6:def3

      func sum Y -> Point of X means 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 ||.(it - ( setsum Y1)).|| < e;

      existence by A1;

      uniqueness

      proof

        let y1,y2 be Point of X such that

         A2: for e1 be Real st e1 > 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 ||.(y1 - ( setsum Y1)).|| < e1 and

         A3: for e2 be Real st e2 > 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 ||.(y2 - ( setsum Y1)).|| < e2;

         A4:

        now

          let e3 be Real such that

           A5: e3 > 0 ;

          set e4 = (e3 / 2);

          consider Y01 be finite Subset of X such that Y01 is non empty and

           A6: Y01 c= Y and

           A7: for Y1 be finite Subset of X st Y01 c= Y1 & Y1 c= Y holds ||.(y1 - ( setsum Y1)).|| < e4 by A2, A5, XREAL_1: 139;

          consider Y02 be finite Subset of X such that Y02 is non empty and

           A8: Y02 c= Y and

           A9: for Y1 be finite Subset of X st Y02 c= Y1 & Y1 c= Y holds ||.(y2 - ( setsum Y1)).|| < e4 by A3, A5, XREAL_1: 139;

          set Y00 = (Y01 \/ Y02);

          

           A10: ((e3 / 2) + (e3 / 2)) = e3 & Y01 c= Y00 by XBOOLE_1: 7;

          

           A11: Y00 c= Y by A6, A8, XBOOLE_1: 8;

          then ||.(y2 - ( setsum Y00)).|| < e4 by A9, XBOOLE_1: 7;

          then ||.( - (y2 - ( setsum Y00))).|| < e4 by BHSP_1: 31;

          then ( ||.(y1 - ( setsum Y00)).|| + ||.( - (y2 - ( setsum Y00))).||) < e3 by A7, A11, A10, XREAL_1: 8;

          then ( ||.((y1 - ( setsum Y00)) + ( - (y2 - ( setsum Y00)))).|| + ( ||.(y1 - ( setsum Y00)).|| + ||.( - (y2 - ( setsum Y00))).||)) < (( ||.(y1 - ( setsum Y00)).|| + ||.( - (y2 - ( setsum Y00))).||) + e3) by BHSP_1: 30, XREAL_1: 8;

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

           ||.(y1 - y2).|| = ||.((y1 - y2) + ( 0. X)).|| by RLVECT_1:def 4

          .= ||.((y1 - y2) + (( setsum Y00) - ( setsum Y00))).|| by RLVECT_1: 5

          .= ||.(((y1 - y2) + ( setsum Y00)) - ( setsum Y00)).|| by RLVECT_1:def 3

          .= ||.((y1 - (y2 - ( setsum Y00))) - ( setsum Y00)).|| by RLVECT_1: 29

          .= ||.(y1 - (( setsum Y00) + (y2 - ( setsum Y00)))).|| by RLVECT_1: 27

          .= ||.((y1 - ( setsum Y00)) - (y2 - ( setsum Y00))).|| by RLVECT_1: 27

          .= ||.((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: 19;

          then

           A13: ||.(y1 - y2).|| <> 0 by BHSP_1: 26;

           0 <= ||.(y1 - y2).|| by BHSP_1: 28;

          hence contradiction by A4, A13;

        end;

        hence thesis;

      end;

    end

    definition

      let X;

      let L be linear-Functional of X;

      :: BHSP_6:def4

      attr L is Lipschitzian means ex K be Real st K > 0 & for x holds |.(L . x).| <= (K * ||.x.||);

    end

    definition

      let X;

      let Y be Subset of X;

      :: BHSP_6:def5

      attr Y is weakly_summable_set means ex x st for L be linear-Functional of X st L is Lipschitzian holds 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 |.(L . (x - ( setsum Y1))).| < e;

    end

    definition

      let X;

      let Y be Subset of X;

      let L be Functional of X;

      :: BHSP_6:def6

      pred Y is_summable_set_by L means ex r be Real st 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 |.(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;

      :: BHSP_6:def7

      func sum_byfunc (Y,L) -> Real means 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 |.(it - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < e;

      existence by A1;

      uniqueness

      proof

        let r1,r2 be Real such that

         A2: for e1 be Real st e1 > 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 |.(r1 - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < e1 and

         A3: for e2 be Real st e2 > 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 |.(r2 - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < e2;

         A4:

        now

          let e3 be Real such that

           A5: e3 > 0 ;

          set e4 = (e3 / 2);

          consider Y01 be finite Subset of X such that Y01 is non empty and

           A6: Y01 c= Y and

           A7: for Y1 be finite Subset of X st Y01 c= Y1 & Y1 c= Y holds |.(r1 - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < e4 by A2, A5, XREAL_1: 139;

          consider Y02 be finite Subset of X such that Y02 is non empty and

           A8: Y02 c= Y and

           A9: for Y1 be finite Subset of X st Y02 c= Y1 & Y1 c= Y holds |.(r2 - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < e4 by A3, A5, XREAL_1: 139;

          set Y00 = (Y01 \/ Y02);

          

           A10: ((e3 / 2) + (e3 / 2)) = e3 & Y01 c= Y00 by XBOOLE_1: 7;

          

           A11: Y00 c= Y by A6, A8, XBOOLE_1: 8;

          then |.(r2 - ( setopfunc (Y00,the carrier of X, REAL ,L, addreal ))).| < e4 by A9, XBOOLE_1: 7;

          then |.((r1 - ( setopfunc (Y00,the carrier of X, REAL ,L, addreal ))) - (r2 - ( setopfunc (Y00,the carrier of X, REAL ,L, addreal )))).| <= ( |.(r1 - ( setopfunc (Y00,the carrier of X, REAL ,L, addreal ))).| + |.(r2 - ( setopfunc (Y00,the carrier of X, REAL ,L, addreal ))).|) & ( |.(r1 - ( setopfunc (Y00,the carrier of X, REAL ,L, addreal ))).| + |.(r2 - ( setopfunc (Y00,the carrier of X, REAL ,L, addreal ))).|) < e3 by A7, A11, A10, COMPLEX1: 57, XREAL_1: 8;

          hence |.(r1 - r2).| < e3 by XXREAL_0: 2;

        end;

        r1 = r2

        proof

          assume

           A12: r1 <> r2;

          

           A13: |.(r1 - r2).| <> 0

          proof

            assume |.(r1 - r2).| = 0 ;

            then (r1 - r2) = 0 by ABSVALUE: 2;

            hence contradiction by A12;

          end;

           0 <= |.(r1 - r2).| by COMPLEX1: 46;

          hence contradiction by A4, A13;

        end;

        hence thesis;

      end;

    end

    theorem :: BHSP_6:3

    

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

      now

        let L be linear-Functional of X;

        assume L is Lipschitzian;

        then

        consider K be Real such that

         A2: 0 < K and

         A3: for x holds |.(L . x).| <= (K * ||.x.||);

        now

          let e1 be Real such that

           A4: 0 < e1;

          set e = (e1 / K);

          consider Y0 be finite Subset of X such that

           A5: Y0 is non empty & Y0 c= Y and

           A6: for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.(x - ( setsum Y1)).|| < e by A1, A2, A4, XREAL_1: 139;

          

           A7: (e * K) = e1 by A2, XCMPLX_1: 87;

          now

            let Y1 be finite Subset of X;

            assume Y0 c= Y1 & Y1 c= Y;

            then (K * ||.(x - ( setsum Y1)).||) < e1 by A2, A7, A6, XREAL_1: 68;

            then ( |.(L . (x - ( setsum Y1))).| + (K * ||.(x - ( setsum Y1)).||)) < ((K * ||.(x - ( setsum Y1)).||) + e1) by A3, XREAL_1: 8;

            then (( |.(L . (x - ( setsum Y1))).| + (K * ||.(x - ( setsum Y1)).||)) - (K * ||.(x - ( setsum Y1)).||)) < (((K * ||.(x - ( setsum Y1)).||) + e1) - (K * ||.(x - ( setsum Y1)).||)) by XREAL_1: 14;

            hence |.(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 |.(L . (x - ( setsum Y1))).| < e1 by A5;

        end;

        hence for e1 be Real st 0 < e1 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 |.(L . (x - ( setsum Y1))).| < e1;

      end;

      hence thesis;

    end;

    theorem :: BHSP_6:4

    

     Th4: for L be linear-Functional of X holds for p be FinSequence of the carrier of X st ( len p) >= 1 holds 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;

      consider f be sequence of the carrier of X such that

       A2: (f . 1) = (p . 1) and

       A3: for n be Nat st 0 <> n & n < ( len p) holds (f . (n + 1)) = (the addF of X . ((f . n),(p . (n + 1)))) and

       A4: (the addF of X "**" p) = (f . ( len p)) by A1, FINSOP_1: 1;

      let q be FinSequence of REAL such that

       A5: ( dom p) = ( dom q) and

       A6: for i st i in ( dom q) holds (q . i) = (L . (p . i));

      ( Seg ( len q)) = ( dom p) by A5, FINSEQ_1:def 3

      .= ( Seg ( len p)) by FINSEQ_1:def 3;

      then

       A7: ( len q) = ( len p) by FINSEQ_1: 6;

      then

      consider g be sequence of REAL such that

       A8: (g . 1) = (q . 1) and

       A9: for n be Nat st 0 <> n & n < ( len q) holds (g . (n + 1)) = ( addreal . ((g . n),(q . (n + 1)))) and

       A10: ( addreal "**" q) = (g . ( len q)) by A1, FINSOP_1: 1;

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len q) implies (g . $1) = (L . (f . $1));

       A11:

      now

        let n;

        

         A12: n in NAT by ORDINAL1:def 12;

        assume

         A13: P[n];

        now

          

           A14: n <= (n + 1) by NAT_1: 11;

          assume that

           A15: 1 <= (n + 1) and

           A16: (n + 1) <= ( len q);

          per cases ;

            suppose

             A17: n = 0 ;

            1 in ( dom p) by A1, FINSEQ_3: 25;

            hence (g . (n + 1)) = (L . (f . (n + 1))) by A5, A6, A2, A8, A17;

          end;

            suppose

             A18: n <> 0 ;

            then

             A19: ( 0 + 1) <= n by INT_1: 7, A12;

            reconsider z = (f . n) as Element of X;

            reconsider z1 = z as VECTOR of X;

            

             A20: (n + 1) in ( dom q) by A15, A16, FINSEQ_3: 25;

            then (p . (n + 1)) in ( rng p) by A5, FUNCT_1: 3;

            then

            reconsider y = (p . (n + 1)) as Element of X;

            reconsider y1 = y as VECTOR of X;

            set Lz = (L . z1), Ly = (L . y1);

            

             A21: ((n + 1) - 1) < (( len q) - 0 ) by A16, XREAL_1: 15;

            

            hence (g . (n + 1)) = ( addreal . ((g . n),(q . (n + 1)))) by A9, A18

            .= ( addreal . ((L . (f . n)),(L . y))) by A6, A13, A16, A14, A19, A20, XXREAL_0: 2

            .= (Lz + Ly) by BINOP_2:def 9

            .= (L . (z1 + y1)) by HAHNBAN:def 2

            .= (L . (f . (n + 1))) by A3, A7, A18, A21;

          end;

        end;

        hence P[(n + 1)];

      end;

      

       A22: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A22, A11);

      hence thesis by A1, A4, A7, A10;

    end;

    theorem :: BHSP_6:5

    

     Th5: for X st the addF of X is commutative associative & the addF of X is having_a_unity holds for S be finite Subset of X st S is non empty holds 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 is having_a_unity;

      let S be finite Subset of X;

      assume S is non empty;

      then

       A2: ( 0 + 1) <= ( card S) by INT_1: 7;

      let L be linear-Functional of X;

      consider p be FinSequence of the carrier of X such that

       A3: p is one-to-one & ( rng p) = S and

       A4: ( setsum S) = (the addF of X "**" p) by A1, Def1;

      reconsider q1 = ( Func_Seq (L,p)) as FinSequence of REAL ;

      

       A5: for i st i in ( dom p) holds (q1 . i) = (L . (p . i))

      proof

        let i such that

         A6: i in ( dom p);

        (q1 . i) = ((L * p) . i) by BHSP_5:def 4

        .= (L . (p . i)) by A6, FUNCT_1: 13;

        hence thesis;

      end;

      

       A7: ( dom L) = the carrier of X by FUNCT_2:def 1;

      now

        let xd be object;

        

         A8: xd in ( dom p) implies (p . xd) in ( rng p) by FUNCT_1: 3;

        xd in ( dom ( Func_Seq (L,p))) iff xd in ( dom (L * p)) by BHSP_5:def 4;

        hence xd in ( dom ( Func_Seq (L,p))) iff xd in ( dom p) by A7, A8, FUNCT_1: 11;

      end;

      then

       A9: ( dom ( Func_Seq (L,p))) = ( dom p) by TARSKI: 2;

      ( len p) >= 1 by A3, A2, FINSEQ_4: 62;

      then (L . (the addF of X "**" p)) = ( addreal "**" q1) by A9, A5, Th4;

      hence thesis by A3, A4, BHSP_5:def 5;

    end;

    theorem :: BHSP_6:6

    

     Th6: for X st the addF of X is commutative associative & the addF of X is having_a_unity holds 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 Lipschitzian holds 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 |.((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 is having_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 Lipschitzian holds 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 |.(L . (x - ( setsum Y1))).| < e;

      take x;

      now

        let L be linear-Functional of X such that

         A3: L is Lipschitzian;

        now

          let e be Real;

          assume e > 0 ;

          then

          consider Y0 be finite Subset of X such that

           A4: Y0 is non empty and

           A5: Y0 c= Y and

           A6: for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds |.(L . (x - ( setsum Y1))).| < e by A2, A3;

          take Y0;

          now

            set x1 = x;

            let Y1 be finite Subset of X such that

             A7: Y0 c= Y1 and

             A8: Y1 c= Y;

            set y1 = ( setsum Y1);

            set r = (L . (x - ( setsum Y1)));

            Y1 <> {} by A4, A7;

            then r = ((L . x1) - (L . y1)) & (L . y1) = ( setopfunc (Y1,the carrier of X, REAL ,L, addreal )) by A1, Th5, HAHNBAN: 19;

            hence |.((L . x) - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < e by A6, A7, A8;

          end;

          hence Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds |.((L . x) - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < e by A4, 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 Y0 c= Y1 & Y1 c= Y holds |.((L . x) - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < e;

      end;

      hence thesis;

    end;

    theorem :: BHSP_6:7

    

     Th7: for X st the addF of X is commutative associative & the addF of X is having_a_unity holds for Y be Subset of X st Y is weakly_summable_set holds for L be linear-Functional of X st L is Lipschitzian holds Y is_summable_set_by L

    proof

      let X such that

       A1: the addF of X is commutative associative & the addF of X is having_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 Lipschitzian holds 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 |.((L . x) - ( setopfunc (Y1,the carrier of X, REAL ,L, addreal ))).| < e by A1, Th6;

      let L be linear-Functional of X;

      assume L is Lipschitzian;

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

      hence thesis;

    end;

    theorem :: BHSP_6:8

    for X st the addF of X is commutative associative & the addF of X is having_a_unity holds for Y be Subset of X st Y is summable_set holds for L be linear-Functional of X st L is Lipschitzian holds Y is_summable_set_by L by Th3, Th7;

    theorem :: BHSP_6:9

    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;

            assume Y c= Y1 & Y1 c= Y;

            then Y1 = Y by XBOOLE_0:def 10;

            then (x - ( setsum Y1)) = ( 0. X) by RLVECT_1: 15;

            hence ||.(x - ( setsum Y1)).|| < e by A2, BHSP_1: 26;

          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;

    end;

    begin

    theorem :: BHSP_6:10

    for X be RealHilbertSpace st the addF of X is commutative associative & the addF of X is having_a_unity holds 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 be RealHilbertSpace such that

       A1: the addF of X is commutative associative & the addF of X is having_a_unity;

      let Y be Subset of X;

       A2:

      now

        defpred P[ object, object] means ex D2 be set st D2 = $2 & ($2 is finite Subset of X & D2 is non empty & D2 c= Y & for z be Real st z = $1 holds for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & D2 misses Y1 holds ||.( setsum Y1).|| < (1 / (z + 1)));

        assume

         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 Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds ||.( setsum Y1).|| < e;

        

         A4: for x be object st x in NAT holds ex y be object st y in ( bool Y) & P[x, y]

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider xx = x as Nat;

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

          ( 0 / (xx + 1)) < (1 / (xx + 1)) by XREAL_1: 74;

          then

          consider Y0 be finite Subset of X such that

           A5: Y0 is non empty & Y0 c= Y and

           A6: for Y1 be finite Subset of X st Y1 is non empty & Y1 c= Y & Y0 misses Y1 holds ||.( setsum Y1).|| < e by A3;

          reconsider Y0 as object;

          take Y0;

          thus Y0 in ( bool Y) by A5;

          take Y0;

          thus thesis by A5, A6;

        end;

        consider B be sequence of ( bool Y) such that

         A7: for x be object st x in NAT holds P[x, (B . x)] from FUNCT_2:sch 1( A4);

        ex A be sequence of ( bool Y) st for i be 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 Nat st i <= j holds (A . i) c= (A . j)

        proof

          

           A8: for x be object 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 holds 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))

          proof

            let x be object;

            assume x in NAT ;

            then P[x, (B . x)] by A7;

            hence thesis;

          end;

          deffunc G( Nat, set) = ((B . ($1 + 1)) \/ $2);

          ex A be Function st ( dom A) = NAT & (A . 0 ) = (B . 0 ) & for n be Nat holds (A . (n + 1)) = G(n,.) from NAT_1:sch 11;

          then

          consider A be Function such that

           A9: ( dom A) = NAT and

           A10: (A . 0 ) = (B . 0 ) and

           A11: for n be Nat holds (A . (n + 1)) = ((B . (n + 1)) \/ (A . n));

          defpred R[ 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 Nat st $1 <= j holds (A . $1) c= (A . j);

           A12:

          now

            let n be Nat such that

             A13: R[n];

            

             A14: 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

               A15: Y1 is non empty & Y1 c= Y and

               A16: (A . (n + 1)) misses Y1;

              (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 thesis by A8, A15;

            end;

            defpred P[ Nat] means (n + 1) <= $1 implies (A . (n + 1)) c= (A . $1);

            

             A17: for j be Nat st P[j] holds P[(j + 1)]

            proof

              let j be Nat such that

               A18: (n + 1) <= j implies (A . (n + 1)) c= (A . j) and

               A19: (n + 1) <= (j + 1);

              per cases ;

                suppose n = j;

                hence thesis;

              end;

                suppose

                 A20: n <> j;

                (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 thesis by A18, A21, NAT_1: 13, XBOOLE_1: 1;

              end;

            end;

            

             A22: P[ 0 ];

            

             A23: for j be Nat holds P[j] from NAT_1:sch 2( A22, A17);

            

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

            thus R[(n + 1)] by A13, A14, A23, XBOOLE_1: 8, A24;

          end;

          for j0 be Nat st j0 = 0 holds for j be Nat st j0 <= j holds (A . j0) c= (A . j)

          proof

            let j0 be Nat such that

             A25: j0 = 0 ;

            defpred P[ Nat] means (j0 <= $1 implies (A . j0) c= (A . $1));

             A26:

            now

              let j be Nat such that

               A27: P[j];

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

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

              hence P[(j + 1)] by A25, A27, XBOOLE_1: 1;

            end;

            

             A28: P[ 0 ];

            thus for j be Nat holds P[j] from NAT_1:sch 2( A28, A26);

          end;

          then

           A29: R[ 0 ] by A8, A10;

          

           A30: for i be Nat holds R[i] from NAT_1:sch 2( A29, A12);

          now

            let y be object;

            assume y in ( rng A);

            then

            consider x be object such that

             A31: x in ( dom A) and

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

            reconsider i = x as Nat by A9, A31;

            (A . i) c= Y by A30;

            hence y in ( bool Y) by A32;

          end;

          then ( rng A) c= ( bool Y) by TARSKI:def 3;

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

          hence thesis by A30;

        end;

        then

        consider A be sequence of ( bool Y) such that

         A33: for i be 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 Nat st i <= j holds (A . i) c= (A . j);

        defpred P[ object, object] means ex Y1 be finite Subset of X st Y1 is non empty & (A . $1) = Y1 & $2 = ( setsum Y1);

        

         A34: for x be object st x in NAT holds ex y be object st y in the carrier of X & P[x, y]

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider i = x as Nat;

          (A . i) is finite Subset of X by A33;

          then

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

          reconsider y = ( setsum Y1) as set;

          (A . i) is non empty by A33;

          then ex Y1 be finite Subset of X st Y1 is non empty set & (A . x) = Y1 & y = ( setsum Y1);

          hence thesis;

        end;

        ex F be sequence of the carrier of X st for x be object st x in NAT holds P[x, (F . x)] from FUNCT_2:sch 1( A34);

        then

        consider F be sequence of the carrier of X such that

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

        now

          let e be Real such that

           A36: e > 0 ;

          

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

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

          proof

            set p = (e / 2);

            consider k1 be Nat such that

             A38: (p " ) < k1 by SEQ_4: 3;

            take k = k1;

            ((p " ) + 0 ) < (k1 + 1) by A38, XREAL_1: 8;

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

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

            hence thesis;

          end;

          then

          consider k be Nat such that

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

          now

            let nn,mm be Nat such that

             A40: nn >= k and

             A41: mm >= k;

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

            then

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

            consider Y2 be finite Subset of X such that Y2 is non empty and

             A42: (A . m) = Y2 and

             A43: (seq . m) = ( setsum Y2) by A35;

            consider Y0 be finite Subset of X such that Y0 is non empty and

             A44: (A . k) = Y0 and

             A45: (seq . k) = ( setsum Y0) by A35;

            

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

            consider Y1 be finite Subset of X such that Y1 is non empty and

             A47: (A . n) = Y1 and

             A48: (seq . n) = ( setsum Y1) by A35;

            

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

            now

              per cases ;

                case

                 A50: Y0 = Y1;

                now

                  per cases ;

                    case Y0 = Y2;

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

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

                  end;

                    case

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

                      

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

                      

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

                      .= Y2 by A46, XBOOLE_1: 12;

                      hence Y02 is non empty by A51;

                      thus Y02 c= Y by A42, A52, XBOOLE_1: 1;

                      thus thesis by XBOOLE_1: 79, A53;

                    end;

                    then

                    consider Y02 be finite Subset of X such that

                     A54: Y02 is non empty & Y02 c= Y and

                     A55: Y02 misses Y0 and

                     A56: (Y0 \/ Y02) = Y2;

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

                    then

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

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

                    

                    then

                     A58: ||.((seq . n) - (seq . m)).|| = ||.((( setsum Y0) - ( setsum Y0)) - ( setsum Y02)).|| by A48, A43, A50, RLVECT_1: 27

                    .= ||.(( 0. X) - ( setsum Y02)).|| by RLVECT_1: 15

                    .= ||.( - ( setsum Y02)).|| by RLVECT_1: 14

                    .= ||.( setsum Y02).|| by BHSP_1: 31;

                    (e * (1 / 2)) < (e * 1) by A36, XREAL_1: 68;

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

                  end;

                end;

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

              end;

                case

                 A59: Y0 <> Y1;

                now

                  per cases ;

                    case Y0 = Y2;

                    then

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

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

                      

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

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

                      .= Y1 by A49, XBOOLE_1: 12;

                      hence thesis by A47, A59, A61, XBOOLE_1: 1, XBOOLE_1: 79;

                    end;

                    then

                    consider Y01 be finite Subset of X such that

                     A62: Y01 is non empty & Y01 c= Y and

                     A63: Y01 misses Y0 and

                     A64: (Y0 \/ Y01) = Y1;

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

                    

                    then

                     A65: ((seq . n) - (seq . k)) = ((seq . k) + (( setsum Y01) + ( - (seq . k)))) by RLVECT_1:def 3

                    .= ((seq . k) - ((seq . k) - ( setsum Y01))) by RLVECT_1: 33

                    .= ((( setsum Y0) - ( setsum Y0)) + ( setsum Y01)) by A45, RLVECT_1: 29

                    .= (( 0. X) + ( setsum Y01)) by RLVECT_1: 5

                    .= ( setsum Y01) by RLVECT_1: 4;

                    ((seq . n) - (seq . m)) = (((seq . n) - (seq . m)) + ( 0. X)) by RLVECT_1: 4

                    .= (((seq . n) - (seq . m)) + ((seq . k) - (seq . k))) by RLVECT_1: 5

                    .= ((seq . n) - ((seq . m) - ((seq . k) - (seq . k)))) by RLVECT_1: 29

                    .= ((seq . n) - (((seq . m) - (seq . k)) + (seq . k))) by RLVECT_1: 29

                    .= ((seq . n) - ((seq . k) - ((seq . k) - (seq . m)))) by RLVECT_1: 33

                    .= (( setsum Y01) + ( 0. X)) by A65, A60, RLVECT_1: 29;

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

                    then

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

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

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

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

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

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

                  end;

                    case

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

                      

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

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

                      .= Y2 by A46, XBOOLE_1: 12;

                      hence thesis by A42, A67, A68, XBOOLE_1: 1, XBOOLE_1: 79;

                    end;

                    then

                    consider Y02 be finite Subset of X such that

                     A69: Y02 is non empty & Y02 c= Y and

                     A70: Y02 misses Y0 and

                     A71: (Y0 \/ Y02) = Y2;

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

                    then

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

                    ex Y01 be finite Subset of X st Y01 is non empty & Y01 c= Y & Y01 misses Y0 & (Y0 \/ Y01) = Y1

                    proof

                      take Y01 = (Y1 \ Y0);

                      

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

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

                      .= Y1 by A49, XBOOLE_1: 12;

                      hence thesis by A47, A59, A73, XBOOLE_1: 1, XBOOLE_1: 79;

                    end;

                    then

                    consider Y01 be finite Subset of X such that

                     A74: Y01 is non empty & Y01 c= Y and

                     A75: Y01 misses Y0 and

                     A76: (Y0 \/ Y01) = Y1;

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

                    

                    then

                     A77: ((seq . n) - (seq . k)) = (( setsum Y01) + ((seq . k) + ( - (seq . k)))) by A45, A48, RLVECT_1:def 3

                    .= (( setsum Y01) + ( 0. X)) by RLVECT_1: 5

                    .= ( setsum Y01) by RLVECT_1: 4;

                    ( setsum Y2) = (( setsum Y0) + ( setsum Y02)) by A1, A70, A71, Th2;

                    

                    then

                     A78: ((seq . m) - (seq . k)) = (( setsum Y02) + ((seq . k) + ( - (seq . k)))) by A45, A43, RLVECT_1:def 3

                    .= (( setsum Y02) + ( 0. X)) by RLVECT_1: 5

                    .= ( setsum Y02) by RLVECT_1: 4;

                    ((seq . n) - (seq . m)) = (((seq . n) - (seq . m)) + ( 0. X)) by RLVECT_1: 4

                    .= (((seq . n) - (seq . m)) + ((seq . k) - (seq . k))) by RLVECT_1: 5

                    .= ((seq . n) - ((seq . m) - ((seq . k) - (seq . k)))) by RLVECT_1: 29

                    .= ((seq . n) - (((seq . m) - (seq . k)) + (seq . k))) by RLVECT_1: 29

                    .= ((seq . n) - ((seq . k) - ((seq . k) - (seq . m)))) by RLVECT_1: 33

                    .= (((seq . n) - (seq . k)) + ((seq . k) + ( - (seq . m)))) by RLVECT_1: 29

                    .= (( setsum Y01) + ( - ( setsum Y02))) by A77, A78, RLVECT_1: 33;

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

                    then

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

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

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

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

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

                  end;

                end;

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

              end;

            end;

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

          end;

          hence ex k be Nat st for n,m be Nat st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < e;

        end;

        then seq is Cauchy by BHSP_3: 2;

        then seq is convergent by BHSP_3:def 4;

        then

        consider x be Point of X such that

         A80: for r be Real st r > 0 holds ex m be Nat st for n be Nat st n >= m holds ||.((seq . n) - x).|| < r by BHSP_2: 9;

        now

          let e be Real such that

           A81: e > 0 ;

          

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

          then

          consider m be Nat such that

           A83: for n be Nat st n >= m holds ||.((seq . n) - x).|| < (e / 2) by A80;

          ex i be Nat st (1 / (i + 1)) < (e / 2) & i >= m

          proof

            set p = (e / 2);

            consider k1 be Nat such that

             A84: (p " ) < k1 by SEQ_4: 3;

            take i = (k1 + m);

            k1 <= (k1 + m) by NAT_1: 11;

            then (p " ) < i by A84, XXREAL_0: 2;

            then ((p " ) + 0 ) < (i + 1) by XREAL_1: 8;

            then (1 / (i + 1)) < (1 / (p " )) by A82, XREAL_1: 76;

            then (1 / (i + 1)) < (1 * ((p " ) " )) by XCMPLX_0:def 9;

            hence thesis by NAT_1: 11;

          end;

          then

          consider i be Nat such that

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

           A86: i >= m;

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

          consider Y0 be finite Subset of X such that

           A87: Y0 is non empty and

           A88: (A . i) = Y0 and

           A89: (seq . i) = ( setsum Y0) by A35;

          

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

          now

            let Y1 be finite Subset of X such that

             A91: Y0 c= Y1 and

             A92: Y1 c= Y;

            now

              per cases ;

                case Y0 = Y1;

                

                then ||.(x - ( setsum Y1)).|| = ||.( - (x - ( setsum Y0))).|| by BHSP_1: 31

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

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

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

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

              end;

                case

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

                  

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

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

                  .= Y1 by A91, XBOOLE_1: 12;

                  hence thesis by A92, A93, A94, XBOOLE_1: 1, XBOOLE_1: 79;

                end;

                then

                consider Y2 be finite Subset of X such that

                 A95: Y2 is non empty & Y2 c= Y and

                 A96: Y0 misses Y2 and

                 A97: (Y0 \/ Y2) = Y1;

                (( setsum Y1) - x) = ((( setsum Y0) + ( setsum Y2)) - x) by A1, A96, A97, Th2

                .= ((( setsum Y0) - x) + ( setsum Y2)) by RLVECT_1:def 3;

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

                then ||.( - (( setsum Y1) - x)).|| <= ( ||.(( setsum Y0) - x).|| + ||.( setsum Y2).||) by BHSP_1: 31;

                then

                 A98: ||.(x + ( - ( setsum Y1))).|| <= ( ||.(( setsum Y0) - x).|| + ||.( setsum Y2).||) by RLVECT_1: 33;

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

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

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

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

              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 A87, A88;

        end;

        hence Y is summable_set;

      end;

      now

        assume Y is summable_set;

        then

        consider x be Point of X such that

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

        now

          let e be Real;

          assume e > 0 ;

          then

          consider Y0 be finite Subset of X such that

           A100: Y0 is non empty and

           A101: Y0 c= Y and

           A102: for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds ||.(x - ( setsum Y1)).|| < (e / 2) by A99, XREAL_1: 139;

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

          now

            let Y1 be finite Subset of X such that Y1 is non empty and

             A103: Y1 c= Y and

             A104: Y0 misses Y1;

            set Z = (Y0 \/ Y1);

            Y0 c= Z by XBOOLE_1: 7;

            then ||.(x - ( setsum Z)).|| < (e / 2) by A101, A102, A103, XBOOLE_1: 8;

            then

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

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

            then

             A106: ||.((x - ( setsum Z)) - (x - ( setsum Y0))).|| <= ( ||.(x - ( setsum Z)).|| + ||.(x - ( setsum Y0)).||) by BHSP_1: 31;

            (( setsum Z) - ( setsum Y0)) = ((( setsum Y1) + ( setsum Y0)) - ( setsum Y0)) by A1, A104, Th2

            .= (( setsum Y1) + (( setsum Y0) + ( - ( setsum Y0)))) by RLVECT_1:def 3

            .= (( setsum Y1) + ( 0. X)) by RLVECT_1: 5

            .= ( setsum Y1) by RLVECT_1: 4;

            

            then ||.( setsum Y1).|| = ||.( - (( setsum Z) - ( setsum Y0))).|| by BHSP_1: 31

            .= ||.(( setsum Y0) - ( setsum Z)).|| by RLVECT_1: 33

            .= ||.(( 0. X) + (( setsum Y0) - ( setsum Z))).|| by RLVECT_1: 4

            .= ||.((x - x) + (( setsum Y0) - ( setsum Z))).|| by RLVECT_1: 5

            .= ||.(x - (x - (( setsum Y0) - ( setsum Z)))).|| by RLVECT_1: 29

            .= ||.(x - ((x - ( setsum Y0)) + ( setsum Z))).|| by RLVECT_1: 29

            .= ||.((x - ( setsum Z)) - (x - ( setsum Y0))).|| by RLVECT_1: 27;

            hence ||.( setsum Y1).|| < e by A106, A105, 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 A101;

        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;

      hence thesis by A2;

    end;