rsspace3.miz



    begin

    definition

      :: RSSPACE3:def1

      func the_set_of_l1RealSequences -> Subset of Linear_Space_of_RealSequences means

      : Def1: for x be object holds x in it iff x in the_set_of_RealSequences & ( seq_id x) is absolutely_summable;

      existence

      proof

        defpred P[ object] means ( seq_id $1) is absolutely_summable;

        consider IT be set such that

         A1: for x be object holds x in IT iff x in the_set_of_RealSequences & P[x] from XBOOLE_0:sch 1;

        for x be object st x in IT holds x in the_set_of_RealSequences by A1;

        then IT is Subset of the_set_of_RealSequences by TARSKI:def 3;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of Linear_Space_of_RealSequences ;

        assume that

         A2: for x be object holds x in X1 iff x in the_set_of_RealSequences & ( seq_id x) is absolutely_summable and

         A3: for x be object holds x in X2 iff x in the_set_of_RealSequences & ( seq_id x) is absolutely_summable;

        for x be object st x in X2 holds x in X1

        proof

          let x be object;

          assume x in X2;

          then x in the_set_of_RealSequences & ( seq_id x) is absolutely_summable by A3;

          hence thesis by A2;

        end;

        then

         A4: X2 c= X1 by TARSKI:def 3;

        for x be object st x in X1 holds x in X2

        proof

          let x be object;

          assume x in X1;

          then x in the_set_of_RealSequences & ( seq_id x) is absolutely_summable by A2;

          hence thesis by A3;

        end;

        then X1 c= X2 by TARSKI:def 3;

        hence thesis by A4, XBOOLE_0:def 10;

      end;

    end

    theorem :: RSSPACE3:1

    

     Th1: for c be Real, seq be Real_Sequence st seq is convergent holds for rseq be Real_Sequence st (for i be Nat holds (rseq . i) = |.((seq . i) - c).|) holds rseq is convergent & ( lim rseq) = |.(( lim seq) - c).|

    proof

      let c be Real;

      reconsider cc = c as Element of REAL by XREAL_0:def 1;

      set cseq = ( seq_const c);

      let seq be Real_Sequence such that

       A1: seq is convergent;

      

       A2: (seq - cseq) is convergent by A1;

      then

       A3: ( abs (seq - cseq)) is convergent;

      let rseq be Real_Sequence such that

       A4: for i be Nat holds (rseq . i) = |.((seq . i) - c).|;

      now

        let i be Nat;

        

        thus (rseq . i) = |.((seq . i) - c).| by A4

        .= |.((seq . i) - (cseq . i)).| by SEQ_1: 57

        .= |.((seq . i) + ( - (cseq . i))).|

        .= |.((seq . i) + (( - cseq) . i)).| by SEQ_1: 10

        .= |.((seq + ( - cseq)) . i).| by SEQ_1: 7

        .= |.((seq - cseq) . i).| by SEQ_1: 11

        .= (( abs (seq - cseq)) . i) by SEQ_1: 12;

      end;

      then

       A5: for x be object st x in NAT holds (rseq . x) = (( abs (seq - cseq)) . x);

      ( lim ( abs (seq - cseq))) = |.( lim (seq - cseq)).| by A2, SEQ_4: 14

      .= |.(( lim seq) - ( lim cseq)).| by A1, SEQ_2: 12

      .= |.(( lim seq) - (cseq . 0 )).| by SEQ_4: 26

      .= |.(( lim seq) - c).| by SEQ_1: 57;

      hence thesis by A5, A3, FUNCT_2: 12;

    end;

    registration

      cluster the_set_of_l1RealSequences -> non empty;

      coherence

      proof

        ( seq_id Zeroseq ) is absolutely_summable

        proof

          reconsider rseq = ( seq_id Zeroseq ) as Real_Sequence;

          for n be Nat holds (rseq . n) = 0 ;

          hence thesis by COMSEQ_3: 3;

        end;

        hence thesis by Def1;

      end;

    end

    registration

      cluster the_set_of_l1RealSequences -> linearly-closed;

      coherence

      proof

        set W = the_set_of_l1RealSequences ;

        

         A1: for v,u be VECTOR of Linear_Space_of_RealSequences st v in the_set_of_l1RealSequences & u in the_set_of_l1RealSequences holds (v + u) in the_set_of_l1RealSequences

        proof

          let v,u be VECTOR of Linear_Space_of_RealSequences such that

           A2: v in W and

           A3: u in W;

          ( seq_id (v + u)) is absolutely_summable

          proof

            set r = ( abs ( seq_id (v + u)));

            set q = ( abs ( seq_id u));

            set p = ( abs ( seq_id v));

            

             A4: for n be Nat holds 0 <= (r . n)

            proof

              let n be Nat;

              (r . n) = |.(( seq_id (v + u)) . n).| by SEQ_1: 12;

              hence thesis by COMPLEX1: 46;

            end;

            

             A5: for n be Nat holds (r . n) <= ((p + q) . n)

            proof

              let n be Nat;

              

               A6: ( |.(( seq_id v) . n).| + |.(( seq_id u) . n).|) = ((( abs ( seq_id v)) . n) + |.(( seq_id u) . n).|) by SEQ_1: 12

              .= ((( abs ( seq_id v)) . n) + (( abs ( seq_id u)) . n)) by SEQ_1: 12

              .= ((p + q) . n) by SEQ_1: 7;

              (r . n) = |.(( seq_id (v + u)) . n).| by SEQ_1: 12

              .= |.(( seq_id (( seq_id v) + ( seq_id u))) . n).| by RSSPACE: 2

              .= |.((( seq_id v) . n) + (( seq_id u) . n)).| by SEQ_1: 7;

              hence thesis by A6, COMPLEX1: 56;

            end;

            ( seq_id u) is absolutely_summable by A3, Def1;

            then

             A7: q is summable by SERIES_1:def 4;

            ( seq_id v) is absolutely_summable by A2, Def1;

            then p is summable by SERIES_1:def 4;

            then (p + q) is summable by A7, SERIES_1: 7;

            then r is summable by A4, A5, SERIES_1: 20;

            hence thesis by SERIES_1:def 4;

          end;

          hence thesis by Def1;

        end;

        for a be Real holds for v be VECTOR of Linear_Space_of_RealSequences st v in W holds (a * v) in W

        proof

          let a be Real;

          let v be VECTOR of Linear_Space_of_RealSequences such that

           A8: v in W;

          ( seq_id (a * v)) is absolutely_summable

          proof

            set r1 = ( |.a.| (#) ( abs ( seq_id v)));

            set q1 = ( abs ( seq_id (a * v)));

            

             A9: for n be Nat holds 0 <= (q1 . n)

            proof

              let n be Nat;

              (q1 . n) = |.(( seq_id (a * v)) . n).| by SEQ_1: 12;

              hence thesis by COMPLEX1: 46;

            end;

            

             A10: for n be Nat holds (q1 . n) <= (r1 . n)

            proof

              let n be Nat;

              (q1 . n) = |.(( seq_id (a * v)) . n).| by SEQ_1: 12

              .= |.(( seq_id (a (#) ( seq_id v))) . n).| by RSSPACE: 3

              .= (( abs (a (#) ( seq_id v))) . n) by SEQ_1: 12;

              hence thesis by SEQ_1: 56;

            end;

            ( seq_id v) is absolutely_summable by A8, Def1;

            then ( abs ( seq_id v)) is summable by SERIES_1:def 4;

            then r1 is summable by SERIES_1: 10;

            then q1 is summable by A9, A10, SERIES_1: 20;

            hence thesis by SERIES_1:def 4;

          end;

          hence thesis by Def1;

        end;

        hence thesis by A1, RLSUB_1:def 1;

      end;

    end

    

     Lm1: RLSStruct (# the_set_of_l1RealSequences , ( Zero_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )), ( Add_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )), ( Mult_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )) #) is Subspace of Linear_Space_of_RealSequences by RSSPACE: 11;

    registration

      cluster RLSStruct (# the_set_of_l1RealSequences , ( Zero_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )), ( Add_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )), ( Mult_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by RSSPACE: 11;

    end

    

     Lm2: RLSStruct (# the_set_of_l1RealSequences , ( Zero_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )), ( Add_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )), ( Mult_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )) #) is RealLinearSpace;

    definition

      :: RSSPACE3:def2

      func l_norm -> Function of the_set_of_l1RealSequences , REAL means

      : Def2: for x be object st x in the_set_of_l1RealSequences holds (it . x) = ( Sum ( abs ( seq_id x)));

      existence

      proof

        deffunc F( object) = ( Sum ( abs ( seq_id $1)));

        

         A1: for z be object st z in the_set_of_l1RealSequences holds F(z) in REAL by XREAL_0:def 1;

        ex f be Function of the_set_of_l1RealSequences , REAL st for x be object st x in the_set_of_l1RealSequences holds (f . x) = F(x) from FUNCT_2:sch 2( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let NORM1,NORM2 be Function of the_set_of_l1RealSequences , REAL such that

         A2: for x be object st x in the_set_of_l1RealSequences holds (NORM1 . x) = ( Sum ( abs ( seq_id x))) and

         A3: for x be object st x in the_set_of_l1RealSequences holds (NORM2 . x) = ( Sum ( abs ( seq_id x)));

        

         A4: for z be object st z in the_set_of_l1RealSequences holds (NORM1 . z) = (NORM2 . z)

        proof

          let z be object such that

           A5: z in the_set_of_l1RealSequences ;

          (NORM1 . z) = ( Sum ( abs ( seq_id z))) by A2, A5;

          hence thesis by A3, A5;

        end;

        ( dom NORM1) = the_set_of_l1RealSequences & ( dom NORM2) = the_set_of_l1RealSequences by FUNCT_2:def 1;

        hence thesis by A4, FUNCT_1: 2;

      end;

    end

    registration

      let X be non empty set, Z be Element of X, A be BinOp of X, M be Function of [: REAL , X:], X, N be Function of X, REAL ;

      cluster NORMSTR (# X, Z, A, M, N #) -> non empty;

      coherence ;

    end

    theorem :: RSSPACE3:2

    for l be NORMSTR st the RLSStruct of l is RealLinearSpace holds l is RealLinearSpace by RSSPACE: 15;

    theorem :: RSSPACE3:3

    

     Th3: for rseq be Real_Sequence st (for n be Nat holds (rseq . n) = 0 ) holds rseq is absolutely_summable & ( Sum ( abs rseq)) = 0

    proof

      let rseq be Real_Sequence such that

       A1: for n be Nat holds (rseq . n) = 0 ;

      

       A2: for n be Nat holds (( abs rseq) . n) = 0

      proof

        let n be Nat;

        (rseq . n) = 0 & (( abs rseq) . n) = |.(rseq . n).| by A1, SEQ_1: 12;

        hence thesis by ABSVALUE: 2;

      end;

      

       A3: for m be Nat holds (( Partial_Sums ( abs rseq)) . m) = 0

      proof

        defpred P[ Nat] means (( abs rseq) . $1) = (( Partial_Sums ( abs rseq)) . $1);

        let m be Nat;

        

         A4: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat such that

           A5: (( abs rseq) . k) = (( Partial_Sums ( abs rseq)) . k);

          

          thus (( abs rseq) . (k + 1)) = ( 0 + (( abs rseq) . (k + 1)))

          .= ((( abs rseq) . k) + (( abs rseq) . (k + 1))) by A2

          .= (( Partial_Sums ( abs rseq)) . (k + 1)) by A5, SERIES_1:def 1;

        end;

        

         A6: P[ 0 ] by SERIES_1:def 1;

        for n be Nat holds P[n] from NAT_1:sch 2( A6, A4);

        

        hence (( Partial_Sums ( abs rseq)) . m) = (( abs rseq) . m)

        .= 0 by A2;

      end;

      

       A7: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((( Partial_Sums ( abs rseq)) . m) - 0 ).| < p

      proof

        let p be Real such that

         A8: 0 < p;

        take 0 ;

        let m be Nat such that 0 <= m;

         |.((( Partial_Sums ( abs rseq)) . m) - 0 ).| = |.( 0 - 0 ).| by A3

        .= 0 by ABSVALUE:def 1;

        hence thesis by A8;

      end;

      then

       A9: ( Partial_Sums ( abs rseq)) is convergent by SEQ_2:def 6;

      then

       A10: ( abs rseq) is summable by SERIES_1:def 2;

      ( lim ( Partial_Sums ( abs rseq))) = 0 by A7, A9, SEQ_2:def 7;

      hence thesis by A10, SERIES_1:def 3, SERIES_1:def 4;

    end;

    theorem :: RSSPACE3:4

    

     Th4: for rseq be Real_Sequence st rseq is absolutely_summable & ( Sum ( abs rseq)) = 0 holds for n be Nat holds (rseq . n) = 0

    proof

      let rseq be Real_Sequence such that

       A1: rseq is absolutely_summable and

       A2: ( Sum ( abs rseq)) = 0 ;

      reconsider arseq = ( abs rseq) as Real_Sequence;

      

       A3: for n be Nat holds 0 <= (( abs rseq) . n)

      proof

        let n be Nat;

         0 <= |.(rseq . n).| by COMPLEX1: 46;

        hence thesis by SEQ_1: 12;

      end;

      

       A4: arseq is summable by A1, SERIES_1:def 4;

      let n be Nat;

      (( abs rseq) . n) = 0 by A2, A4, A3, RSSPACE: 17;

      then |.(rseq . n).| = 0 by SEQ_1: 12;

      hence thesis by ABSVALUE: 2;

    end;

    theorem :: RSSPACE3:5

    

     Th5: NORMSTR (# the_set_of_l1RealSequences , ( Zero_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )), ( Add_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )), ( Mult_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )), l_norm #) is RealLinearSpace by Lm2, RSSPACE: 15;

    definition

      :: RSSPACE3:def3

      func l1_Space -> non empty NORMSTR equals NORMSTR (# the_set_of_l1RealSequences , ( Zero_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )), ( Add_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )), ( Mult_ ( the_set_of_l1RealSequences , Linear_Space_of_RealSequences )), l_norm #);

      coherence ;

    end

    begin

    theorem :: RSSPACE3:6

    

     Th6: the carrier of l1_Space = the_set_of_l1RealSequences & (for x be set holds x is VECTOR of l1_Space iff x is Real_Sequence & ( seq_id x) is absolutely_summable) & ( 0. l1_Space ) = Zeroseq & (for u be VECTOR of l1_Space holds u = ( seq_id u)) & (for u,v be VECTOR of l1_Space holds (u + v) = (( seq_id u) + ( seq_id v))) & (for r be Real holds for u be VECTOR of l1_Space holds (r * u) = (r (#) ( seq_id u))) & (for u be VECTOR of l1_Space holds ( - u) = ( - ( seq_id u)) & ( seq_id ( - u)) = ( - ( seq_id u))) & (for u,v be VECTOR of l1_Space holds (u - v) = (( seq_id u) - ( seq_id v))) & (for v be VECTOR of l1_Space holds ( seq_id v) is absolutely_summable) & for v be VECTOR of l1_Space holds ||.v.|| = ( Sum ( abs ( seq_id v)))

    proof

      set l1 = l1_Space ;

      

       A1: for x be set holds x is Element of l1 iff x is Real_Sequence & ( seq_id x) is absolutely_summable

      proof

        let x be set;

        x in the_set_of_RealSequences iff x is Real_Sequence by FUNCT_2: 8, FUNCT_2: 66;

        hence thesis by Def1;

      end;

      

       A2: for u,v be VECTOR of l1 holds (u + v) = (( seq_id u) + ( seq_id v))

      proof

        let u,v be VECTOR of l1;

        reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_RealSequences by Lm1, RLSUB_1: 10;

        set L1 = Linear_Space_of_RealSequences ;

        set W = the_set_of_l1RealSequences ;

        ( dom the addF of L1) = [:the carrier of L1, the carrier of L1:] by FUNCT_2:def 1;

        then ( dom (the addF of Linear_Space_of_RealSequences || W)) = [:W, W:] by RELAT_1: 62, ZFMISC_1: 96;

        then

         A3: [u, v] in ( dom (the addF of Linear_Space_of_RealSequences || W)) by ZFMISC_1: 87;

        (u + v) = ((the addF of Linear_Space_of_RealSequences || W) . [u, v]) by RSSPACE:def 8

        .= (u1 + v1) by A3, FUNCT_1: 47;

        hence thesis by RSSPACE: 2;

      end;

      

       A4: for r be Real holds for u be VECTOR of l1 holds (r * u) = (r (#) ( seq_id u))

      proof

        let r be Real;

        let u be VECTOR of l1;

        reconsider r as Element of REAL by XREAL_0:def 1;

        reconsider u1 = u as VECTOR of Linear_Space_of_RealSequences by Lm1, RLSUB_1: 10;

        set L1 = Linear_Space_of_RealSequences ;

        set W = the_set_of_l1RealSequences ;

        ( dom the Mult of L1) = [: REAL , the carrier of L1:] by FUNCT_2:def 1;

        then ( dom (the Mult of Linear_Space_of_RealSequences | [: REAL , W:])) = [: REAL , W:] by RELAT_1: 62, ZFMISC_1: 96;

        then

         A5: [r, u] in ( dom (the Mult of Linear_Space_of_RealSequences | [: REAL , W:])) by ZFMISC_1: 87;

        (r * u) = ((the Mult of Linear_Space_of_RealSequences | [: REAL , W:]) . [r, u]) by RSSPACE:def 9

        .= (r * u1) by A5, FUNCT_1: 47;

        hence thesis by RSSPACE: 3;

      end;

      

       A6: for u be VECTOR of l1 holds u = ( seq_id u)

      proof

        let u be VECTOR of l1;

        u is VECTOR of Linear_Space_of_RealSequences by Lm1, RLSUB_1: 10;

        hence thesis;

      end;

      

       A7: for u be VECTOR of l1 holds ( - u) = ( - ( seq_id u)) & ( seq_id ( - u)) = ( - ( seq_id u))

      proof

        let u be VECTOR of l1;

        ( - u) = (( - 1) * u) by Th5, RLVECT_1: 16

        .= (( - 1) (#) ( seq_id u)) by A4

        .= ( - ( seq_id u)) by SEQ_1: 17;

        hence thesis;

      end;

      

       A8: for u,v be VECTOR of l1 holds (u - v) = (( seq_id u) - ( seq_id v))

      proof

        let u,v be VECTOR of l1;

        

        thus (u - v) = (( seq_id u) + ( seq_id ( - v))) by A2

        .= (( seq_id u) + ( - ( seq_id v))) by A7

        .= (( seq_id u) - ( seq_id v)) by SEQ_1: 11;

      end;

      

       A9: for v be VECTOR of l1 holds ||.v.|| = ( Sum ( abs ( seq_id v))) by Def2;

      ( 0. l1) = ( 0. Linear_Space_of_RealSequences ) by RSSPACE:def 10

      .= Zeroseq ;

      hence thesis by A1, A6, A2, A4, A7, A8, A9;

    end;

    theorem :: RSSPACE3:7

    

     Th7: for x,y be Point of l1_Space , a be Real holds ( ||.x.|| = 0 iff x = ( 0. l1_Space )) & 0 <= ||.x.|| & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) & ||.(a * x).|| = ( |.a.| * ||.x.||)

    proof

      let x,y be Point of l1_Space ;

      let a be Real;

      

       A1: for n be Nat holds 0 <= (( abs ( seq_id x)) . n)

      proof

        let n be Nat;

         0 <= |.(( seq_id x) . n).| by COMPLEX1: 46;

        hence thesis by SEQ_1: 12;

      end;

       A2:

      now

        let n be Nat;

        (( abs ( seq_id (x + y))) . n) = |.(( seq_id (x + y)) . n).| by SEQ_1: 12;

        hence 0 <= (( abs ( seq_id (x + y))) . n) by COMPLEX1: 46;

      end;

      

       A3: for n be Nat holds (( abs ( seq_id (x + y))) . n) = |.((( seq_id x) . n) + (( seq_id y) . n)).|

      proof

        let n be Nat;

        (( abs ( seq_id (x + y))) . n) = (( abs ( seq_id (( seq_id x) + ( seq_id y)))) . n) by Th6

        .= |.((( seq_id x) + ( seq_id y)) . n).| by SEQ_1: 12

        .= |.((( seq_id x) . n) + (( seq_id y) . n)).| by SEQ_1: 7;

        hence thesis;

      end;

      

       A4: for n be Nat holds (( abs ( seq_id (x + y))) . n) <= ((( abs ( seq_id x)) . n) + (( abs ( seq_id y)) . n))

      proof

        let n be Nat;

         |.((( seq_id x) . n) + (( seq_id y) . n)).| <= ( |.(( seq_id x) . n).| + |.(( seq_id y) . n).|) by COMPLEX1: 56;

        then (( abs ( seq_id (x + y))) . n) <= ( |.(( seq_id x) . n).| + |.(( seq_id y) . n).|) by A3;

        then (( abs ( seq_id (x + y))) . n) <= ((( abs ( seq_id x)) . n) + |.(( seq_id y) . n).|) by SEQ_1: 12;

        hence thesis by SEQ_1: 12;

      end;

      

       A5: for n be Nat holds (( abs ( seq_id (x + y))) . n) <= ((( abs ( seq_id x)) + ( abs ( seq_id y))) . n)

      proof

        let n be Nat;

        ((( abs ( seq_id x)) . n) + (( abs ( seq_id y)) . n)) = ((( abs ( seq_id x)) + ( abs ( seq_id y))) . n) by SEQ_1: 7;

        hence thesis by A4;

      end;

      ( seq_id y) is absolutely_summable by Def1;

      then

       A6: ( abs ( seq_id y)) is summable by SERIES_1:def 4;

      ( seq_id x) is absolutely_summable by Def1;

      then ( abs ( seq_id x)) is summable by SERIES_1:def 4;

      then (( abs ( seq_id x)) + ( abs ( seq_id y))) is summable by A6, SERIES_1: 7;

      then

       A7: ( Sum ( abs ( seq_id (x + y)))) <= ( Sum (( abs ( seq_id x)) + ( abs ( seq_id y)))) by A5, A2, SERIES_1: 20;

       A8:

      now

        assume x = ( 0. l1_Space );

        then

         A9: for n be Nat holds (( seq_id x) . n) = 0 by Th6;

        

        thus ||.x.|| = ( Sum ( abs ( seq_id x))) by Def2

        .= 0 by A9, Th3;

      end;

      

       A10: ( Sum ( abs ( seq_id (x + y)))) = ||.(x + y).|| by Th6;

       A11:

      now

        

         A12: x in the_set_of_RealSequences by Def1;

        assume

         A13: ||.x.|| = 0 ;

         ||.x.|| = ( Sum ( abs ( seq_id x))) & ( seq_id x) is absolutely_summable by Th6;

        then for n be Nat holds 0 = (( seq_id x) . n) by A13, Th4;

        hence x = ( 0. l1_Space ) by A12, Th6, RSSPACE: 5;

      end;

      

       A14: ||.x.|| = ( Sum ( abs ( seq_id x))) & ||.y.|| = ( Sum ( abs ( seq_id y))) by Th6;

      

       A15: for n be Nat holds (( abs (a (#) ( seq_id x))) . n) = ( |.a.| * (( abs ( seq_id x)) . n))

      proof

        let n be Nat;

        (( abs (a (#) ( seq_id x))) . n) = |.((a (#) ( seq_id x)) . n).| by SEQ_1: 12

        .= |.(a * (( seq_id x) . n)).| by SEQ_1: 9

        .= ( |.a.| * |.(( seq_id x) . n).|) by COMPLEX1: 65

        .= ( |.a.| * (( abs ( seq_id x)) . n)) by SEQ_1: 12;

        hence thesis;

      end;

      ( seq_id x) is absolutely_summable by Def1;

      then

       A16: ( abs ( seq_id x)) is summable by SERIES_1:def 4;

      ( seq_id x) is absolutely_summable by Def1;

      then

       A17: ( abs ( seq_id x)) is summable by SERIES_1:def 4;

       ||.(a * x).|| = ( Sum ( abs ( seq_id (a * x)))) by Th6

      .= ( Sum |.( seq_id (a (#) ( seq_id x))).|) by Th6

      .= ( Sum ( |.a.| (#) ( abs ( seq_id x)))) by A15, SEQ_1: 9

      .= ( |.a.| * ( Sum ( abs ( seq_id x)))) by A16, SERIES_1: 10

      .= ( |.a.| * ||.x.||) by Th6;

      hence thesis by A11, A8, A1, A17, A14, A10, A6, A7, SERIES_1: 7, SERIES_1: 18;

    end;

    registration

      cluster l1_Space -> reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable;

      coherence by Th7, Lm2, NORMSP_1:def 1, RSSPACE: 15;

    end

    

     Lm3: for c be Real, seq,seq1 be Real_Sequence st seq is convergent & seq1 is convergent holds for rseq be Real_Sequence st (for i be Nat holds (rseq . i) = ( |.((seq . i) - c).| + (seq1 . i))) holds rseq is convergent & ( lim rseq) = ( |.(( lim seq) - c).| + ( lim seq1))

    proof

      let c be Real;

      let seq,seq1 be Real_Sequence such that

       A1: seq is convergent and

       A2: seq1 is convergent;

      reconsider cc = c as Element of REAL by XREAL_0:def 1;

      set cseq = ( seq_const c);

      

       A3: (seq - cseq) is convergent by A1;

      then

       A4: ( abs (seq - cseq)) is convergent;

      let rseq be Real_Sequence such that

       A5: for i be Nat holds (rseq . i) = ( |.((seq . i) - c).| + (seq1 . i));

      now

        let i be Element of NAT ;

        

        thus (rseq . i) = ( |.((seq . i) - c).| + (seq1 . i)) by A5

        .= ( |.((seq . i) - (cseq . i)).| + (seq1 . i)) by SEQ_1: 57

        .= ( |.((seq . i) + ( - (cseq . i))).| + (seq1 . i))

        .= ( |.((seq . i) + (( - cseq) . i)).| + (seq1 . i)) by SEQ_1: 10

        .= ( |.((seq + ( - cseq)) . i).| + (seq1 . i)) by SEQ_1: 7

        .= ( |.((seq - cseq) . i).| + (seq1 . i)) by SEQ_1: 11

        .= ((( abs (seq - cseq)) . i) + (seq1 . i)) by SEQ_1: 12

        .= ((( abs (seq - cseq)) + seq1) . i) by SEQ_1: 7;

      end;

      then

       A6: rseq = (( abs (seq - cseq)) + seq1) by FUNCT_2: 63;

      ( lim ( abs (seq - cseq))) = |.( lim (seq - cseq)).| by A3, SEQ_4: 14

      .= |.(( lim seq) - ( lim cseq)).| by A1, SEQ_2: 12

      .= |.(( lim seq) - (cseq . 0 )).| by SEQ_4: 26

      .= |.(( lim seq) - c).| by SEQ_1: 57;

      hence thesis by A2, A6, A4, SEQ_2: 6;

    end;

    definition

      let X be non empty NORMSTR, x,y be Point of X;

      :: RSSPACE3:def4

      func dist (x,y) -> Real equals ||.(x - y).||;

      coherence ;

    end

    reserve NRM for non empty RealNormSpace;

    reserve seq for sequence of NRM;

    definition

      let NRM be non empty NORMSTR;

      let seqt be sequence of NRM;

      :: RSSPACE3:def5

      attr seqt is CCauchy means for r1 be Real st r1 > 0 holds ex k1 be Nat st for n1,m1 be Nat st n1 >= k1 & m1 >= k1 holds ( dist ((seqt . n1),(seqt . m1))) < r1;

    end

    notation

      let NRM be non empty NORMSTR;

      let seqt be sequence of NRM;

      synonym seqt is Cauchy_sequence_by_Norm for seqt is CCauchy;

    end

    theorem :: RSSPACE3:8

    

     Th8: seq is Cauchy_sequence_by_Norm iff for r be Real st r > 0 holds ex k be Nat st for n,m be Nat st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r

    proof

      thus seq is Cauchy_sequence_by_Norm implies for r be Real st r > 0 holds ex k be Nat st for n,m be Nat st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r

      proof

        assume

         A1: seq is Cauchy_sequence_by_Norm;

        let r be Real;

        assume r > 0 ;

        then

        consider k be Nat such that

         A2: for n,m be Nat st n >= k & m >= k holds ( dist ((seq . n),(seq . m))) < r by A1;

        for n,m be Nat st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r

        proof

          let n,m be Nat;

          assume n >= k & m >= k;

          then ( dist ((seq . n),(seq . m))) < r by A2;

          hence thesis;

        end;

        hence thesis;

      end;

      assume

       A3: for r be Real st r > 0 holds ex k be Nat st for n,m be Nat st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r;

      now

        let r be Real;

        assume

         A4: r > 0 ;

        now

          consider k be Nat such that

           A5: for n,m be Nat st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r by A3, A4;

          for n,m be Nat st n >= k & m >= k holds ( dist ((seq . n),(seq . m))) < r by A5;

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

        end;

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

      end;

      hence thesis;

    end;

    theorem :: RSSPACE3:9

    for vseq be sequence of l1_Space st vseq is Cauchy_sequence_by_Norm holds vseq is convergent

    proof

      let vseq be sequence of l1_Space such that

       A1: vseq is Cauchy_sequence_by_Norm;

      defpred P[ object, object] means ex i be Nat st $1 = i & ex rseqi be Real_Sequence st (for n be Nat holds (rseqi . n) = (( seq_id (vseq . n)) . i)) & rseqi is convergent & $2 = ( lim rseqi);

      

       A2: for x be object st x in NAT holds ex y be object st y in REAL & P[x, y]

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Nat;

        deffunc F( Nat) = (( seq_id (vseq . $1)) . i);

        consider rseqi be Real_Sequence such that

         A3: for n be Nat holds (rseqi . n) = F(n) from SEQ_1:sch 1;

        reconsider lr = ( lim rseqi) as Element of REAL by XREAL_0:def 1;

        take lr;

        now

          let e be Real such that

           A4: e > 0 ;

          thus ex k be Nat st for m be Nat st k <= m holds |.((rseqi . m) - (rseqi . k)).| < e

          proof

            consider k be Nat such that

             A5: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A1, A4, Th8;

            for m be Nat st k <= m holds |.((rseqi . m) - (rseqi . k)).| < e

            proof

              let m be Nat such that

               A6: k <= m;

              

               A7: for i be Nat holds 0 <= ( |.( seq_id ((vseq . m) - (vseq . k))).| . i)

              proof

                let i be Nat;

                 0 <= |.(( seq_id ((vseq . m) - (vseq . k))) . i).| by COMPLEX1: 46;

                hence thesis by SEQ_1: 12;

              end;

              ( seq_id ((vseq . m) - (vseq . k))) is absolutely_summable by Def1;

              then ( abs ( seq_id ((vseq . m) - (vseq . k)))) is summable by SERIES_1:def 4;

              then

               A8: (( abs ( seq_id ((vseq . m) - (vseq . k)))) . i) <= ( Sum |.( seq_id ((vseq . m) - (vseq . k))).|) by A7, RSSPACE2: 3;

              ( seq_id ((vseq . m) - (vseq . k))) = ( seq_id (( seq_id (vseq . m)) - ( seq_id (vseq . k)))) by Th6

              .= (( seq_id (vseq . m)) + ( - ( seq_id (vseq . k)))) by SEQ_1: 11;

              

              then (( seq_id ((vseq . m) - (vseq . k))) . i) = ((( seq_id (vseq . m)) . i) + (( - ( seq_id (vseq . k))) . i)) by SEQ_1: 7

              .= ((( seq_id (vseq . m)) . i) + ( - (( seq_id (vseq . k)) . i))) by SEQ_1: 10

              .= ((( seq_id (vseq . m)) . i) - (( seq_id (vseq . k)) . i))

              .= ((rseqi . m) - (( seq_id (vseq . k)) . i)) by A3

              .= ((rseqi . m) - (rseqi . k)) by A3;

              then

               A9: |.((rseqi . m) - (rseqi . k)).| = (( abs ( seq_id ((vseq . m) - (vseq . k)))) . i) by SEQ_1: 12;

               ||.((vseq . m) - (vseq . k)).|| = ( Sum |.( seq_id ((vseq . m) - (vseq . k))).|) by Th6;

              then ( Sum |.( seq_id ((vseq . m) - (vseq . k))).|) < e by A5, A6;

              hence thesis by A8, A9, XXREAL_0: 2;

            end;

            hence thesis;

          end;

        end;

        then rseqi is convergent by SEQ_4: 41;

        hence thesis by A3;

      end;

      consider f be sequence of REAL such that

       A10: for x be object st x in NAT holds P[x, (f . x)] from FUNCT_2:sch 1( A2);

      reconsider tseq = f as Real_Sequence;

       A11:

      now

        let i be Nat;

        reconsider x = i as set;

        i in NAT by ORDINAL1:def 12;

        then ex i0 be Nat st x = i0 & ex rseqi be Real_Sequence st (for n be Nat holds (rseqi . n) = (( seq_id (vseq . n)) . i0)) & rseqi is convergent & (f . x) = ( lim rseqi) by A10;

        hence ex rseqi be Real_Sequence st (for n be Nat holds (rseqi . n) = (( seq_id (vseq . n)) . i)) & rseqi is convergent & (tseq . i) = ( lim rseqi);

      end;

      

       A12: for e be Real st e > 0 holds ex k be Nat st for n be Nat st n >= k holds ( abs (( seq_id tseq) - ( seq_id (vseq . n)))) is summable & ( Sum ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) < e

      proof

        let e1 be Real such that

         A13: e1 > 0 ;

        reconsider e1 as Real;

        set e = (e1 / 2);

        

         A14: e < e1 by A13, XREAL_1: 216;

        e > 0 by A13, XREAL_1: 215;

        then

        consider k be Nat such that

         A15: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A1, Th8;

        

         A16: for m,n be Nat st n >= k & m >= k holds (( abs ( seq_id ((vseq . n) - (vseq . m)))) is summable & ( Sum ( abs ( seq_id ((vseq . n) - (vseq . m))))) < e & for i be Nat holds 0 <= (( abs ( seq_id ((vseq . n) - (vseq . m)))) . i))

        proof

          let m,n be Nat;

          assume n >= k & m >= k;

          then ||.((vseq . n) - (vseq . m)).|| < e by A15;

          then

           A17: (the normF of l1_Space . ((vseq . n) - (vseq . m))) < e;

          

           A18: for i be Nat holds 0 <= (( abs ( seq_id ((vseq . n) - (vseq . m)))) . i)

          proof

            let i be Nat;

             0 <= |.(( seq_id ((vseq . n) - (vseq . m))) . i).| by COMPLEX1: 46;

            hence thesis by SEQ_1: 12;

          end;

          ( seq_id ((vseq . n) - (vseq . m))) is absolutely_summable by Def1;

          hence thesis by A17, A18, Def2, SERIES_1:def 4;

        end;

        

         A19: for n be Nat holds for i be Nat holds for rseq be Real_Sequence st (for m be Nat holds (rseq . m) = (( Partial_Sums ( abs ( seq_id ((vseq . m) - (vseq . n))))) . i)) holds rseq is convergent & ( lim rseq) = (( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) . i)

        proof

          let n be Nat;

          defpred P[ Nat] means for rseq be Real_Sequence st for m be Nat holds (rseq . m) = (( Partial_Sums ( abs ( seq_id ((vseq . m) - (vseq . n))))) . $1) holds rseq is convergent & ( lim rseq) = (( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) . $1);

          

           A20: for m,k be Nat holds ( seq_id ((vseq . m) - (vseq . k))) = (( seq_id (vseq . m)) - ( seq_id (vseq . k)))

          proof

            let m,k be Nat;

            ( seq_id ((vseq . m) - (vseq . k))) = ( seq_id (( seq_id (vseq . m)) - ( seq_id (vseq . k)))) by Th6;

            hence thesis;

          end;

          now

            let i be Nat such that

             A21: for rseq be Real_Sequence st (for m be Nat holds (rseq . m) = (( Partial_Sums ( abs ( seq_id ((vseq . m) - (vseq . n))))) . i)) holds rseq is convergent & ( lim rseq) = (( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) . i);

            thus for rseq be Real_Sequence st (for m be Nat holds (rseq . m) = (( Partial_Sums ( abs ( seq_id ((vseq . m) - (vseq . n))))) . (i + 1))) holds rseq is convergent & ( lim rseq) = (( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) . (i + 1))

            proof

              deffunc F( Nat) = (( Partial_Sums ( abs ( seq_id ((vseq . $1) - (vseq . n))))) . i);

              consider rseqb be Real_Sequence such that

               A22: for m be Nat holds (rseqb . m) = F(m) from SEQ_1:sch 1;

              consider rseq0 be Real_Sequence such that

               A23: for m be Nat holds (rseq0 . m) = (( seq_id (vseq . m)) . (i + 1)) and

               A24: rseq0 is convergent and

               A25: (tseq . (i + 1)) = ( lim rseq0) by A11;

              let rseq be Real_Sequence such that

               A26: for m be Nat holds (rseq . m) = (( Partial_Sums ( abs ( seq_id ((vseq . m) - (vseq . n))))) . (i + 1));

               A27:

              now

                let m be Nat;

                

                thus (rseq . m) = (( Partial_Sums ( abs ( seq_id ((vseq . m) - (vseq . n))))) . (i + 1)) by A26

                .= ((( abs ( seq_id ((vseq . m) - (vseq . n)))) . (i + 1)) + (( Partial_Sums ( abs ( seq_id ((vseq . m) - (vseq . n))))) . i)) by SERIES_1:def 1

                .= ((( abs (( seq_id (vseq . m)) - ( seq_id (vseq . n)))) . (i + 1)) + (( Partial_Sums ( abs ( seq_id ((vseq . m) - (vseq . n))))) . i)) by A20

                .= ((( abs (( seq_id (vseq . m)) - ( seq_id (vseq . n)))) . (i + 1)) + (rseqb . m)) by A22

                .= ( |.((( seq_id (vseq . m)) - ( seq_id (vseq . n))) . (i + 1)).| + (rseqb . m)) by SEQ_1: 12

                .= ( |.((( seq_id (vseq . m)) + ( - ( seq_id (vseq . n)))) . (i + 1)).| + (rseqb . m)) by SEQ_1: 11

                .= ( |.((( seq_id (vseq . m)) . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1))).| + (rseqb . m)) by SEQ_1: 7

                .= ( |.((( seq_id (vseq . m)) . (i + 1)) + ( - (( seq_id (vseq . n)) . (i + 1)))).| + (rseqb . m)) by SEQ_1: 10

                .= ( |.((( seq_id (vseq . m)) . (i + 1)) - (( seq_id (vseq . n)) . (i + 1))).| + (rseqb . m))

                .= ( |.((rseq0 . m) - (( seq_id (vseq . n)) . (i + 1))).| + (rseqb . m)) by A23;

              end;

              

               A28: rseqb is convergent by A21, A22;

              

              then ( lim rseq) = ( |.(( lim rseq0) - (( seq_id (vseq . n)) . (i + 1))).| + ( lim rseqb)) by A24, A27, Lm3

              .= ( |.((tseq . (i + 1)) + ( - (( seq_id (vseq . n)) . (i + 1)))).| + ( lim rseqb)) by A25

              .= ( |.((tseq . (i + 1)) + (( - ( seq_id (vseq . n))) . (i + 1))).| + ( lim rseqb)) by SEQ_1: 10

              .= ( |.((tseq + ( - ( seq_id (vseq . n)))) . (i + 1)).| + ( lim rseqb)) by SEQ_1: 7

              .= ( |.((tseq - ( seq_id (vseq . n))) . (i + 1)).| + ( lim rseqb)) by SEQ_1: 11

              .= ((( abs (tseq - ( seq_id (vseq . n)))) . (i + 1)) + ( lim rseqb)) by SEQ_1: 12

              .= ((( abs (tseq - ( seq_id (vseq . n)))) . (i + 1)) + (( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) . i)) by A21, A22

              .= (( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) . (i + 1)) by SERIES_1:def 1;

              hence thesis by A28, A24, A27, Lm3;

            end;

          end;

          then

           A29: for i be Nat st P[i] holds P[(i + 1)];

          now

            let rseq be Real_Sequence such that

             A30: for m be Nat holds (rseq . m) = (( Partial_Sums ( abs ( seq_id ((vseq . m) - (vseq . n))))) . 0 );

            thus rseq is convergent & ( lim rseq) = (( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) . 0 )

            proof

              consider rseq0 be Real_Sequence such that

               A31: for m be Nat holds (rseq0 . m) = (( seq_id (vseq . m)) . 0 ) and

               A32: rseq0 is convergent and

               A33: (tseq . 0 ) = ( lim rseq0) by A11;

              

               A34: for m be Nat holds (rseq . m) = |.((rseq0 . m) - (( seq_id (vseq . n)) . 0 )).|

              proof

                let m be Nat;

                (rseq . m) = (( Partial_Sums ( abs ( seq_id ((vseq . m) - (vseq . n))))) . 0 ) by A30

                .= (( abs ( seq_id ((vseq . m) - (vseq . n)))) . 0 ) by SERIES_1:def 1

                .= (( abs (( seq_id (vseq . m)) - ( seq_id (vseq . n)))) . 0 ) by A20

                .= (( abs (( seq_id (vseq . m)) + ( - ( seq_id (vseq . n))))) . 0 ) by SEQ_1: 11

                .= |.((( seq_id (vseq . m)) + ( - ( seq_id (vseq . n)))) . 0 ).| by SEQ_1: 12

                .= |.((( seq_id (vseq . m)) . 0 ) + (( - ( seq_id (vseq . n))) . 0 )).| by SEQ_1: 7

                .= |.((( seq_id (vseq . m)) . 0 ) + ( - (( seq_id (vseq . n)) . 0 ))).| by SEQ_1: 10

                .= |.((( seq_id (vseq . m)) . 0 ) - (( seq_id (vseq . n)) . 0 )).|;

                hence thesis by A31;

              end;

              

              then ( lim rseq) = |.(( lim rseq0) - (( seq_id (vseq . n)) . 0 )).| by A32, Th1

              .= |.((tseq . 0 ) + ( - (( seq_id (vseq . n)) . 0 ))).| by A33

              .= |.((tseq . 0 ) + (( - ( seq_id (vseq . n))) . 0 )).| by SEQ_1: 10

              .= |.((tseq + ( - ( seq_id (vseq . n)))) . 0 ).| by SEQ_1: 7

              .= |.((tseq - ( seq_id (vseq . n))) . 0 ).| by SEQ_1: 11

              .= (( abs (( seq_id tseq) - ( seq_id (vseq . n)))) . 0 ) by SEQ_1: 12

              .= (( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) . 0 ) by SERIES_1:def 1;

              hence thesis by A32, A34, Th1;

            end;

          end;

          then

           A35: P[ 0 ];

          for i be Nat holds P[i] from NAT_1:sch 2( A35, A29);

          hence thesis;

        end;

        for n be Nat st n >= k holds ( abs (( seq_id tseq) - ( seq_id (vseq . n)))) is summable & ( Sum ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) < e1

        proof

          let n be Nat such that

           A36: n >= k;

          

           A37: for i be Nat st 0 <= i holds (( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) . i) <= e

          proof

            let i be Nat such that 0 <= i;

            deffunc F( Nat) = (( Partial_Sums ( abs ( seq_id ((vseq . $1) - (vseq . n))))) . i);

            consider rseq be Real_Sequence such that

             A38: for m be Nat holds (rseq . m) = F(m) from SEQ_1:sch 1;

            

             A39: for m be Nat st m >= k holds (rseq . m) <= e

            proof

              let m be Nat;

              

               A40: (rseq . m) = (( Partial_Sums ( abs ( seq_id ((vseq . m) - (vseq . n))))) . i) by A38;

              assume

               A41: m >= k;

              then ( abs ( seq_id ((vseq . m) - (vseq . n)))) is summable & for i be Nat holds 0 <= (( abs ( seq_id ((vseq . m) - (vseq . n)))) . i) by A16, A36;

              then

               A42: (( Partial_Sums ( abs ( seq_id ((vseq . m) - (vseq . n))))) . i) <= ( Sum ( abs ( seq_id ((vseq . m) - (vseq . n))))) by RSSPACE2: 3;

              ( Sum ( abs ( seq_id ((vseq . m) - (vseq . n))))) < e by A16, A36, A41;

              hence thesis by A42, A40, XXREAL_0: 2;

            end;

            rseq is convergent & ( lim rseq) = (( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) . i) by A19, A38;

            hence thesis by A39, RSSPACE2: 5;

          end;

          now

            take e1;

            let i be Nat;

            (( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) . i) <= e by A37, NAT_1: 2;

            hence (( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) . i) < e1 by A14, XXREAL_0: 2;

          end;

          then

           A43: ( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) is bounded_above by SEQ_2:def 3;

          

           A44: for i be Nat holds 0 <= (( abs (( seq_id tseq) - ( seq_id (vseq . n)))) . i)

          proof

            let i be Nat;

            (( abs (( seq_id tseq) - ( seq_id (vseq . n)))) . i) = |.((( seq_id tseq) - ( seq_id (vseq . n))) . i).| by SEQ_1: 12;

            hence thesis by COMPLEX1: 46;

          end;

          then ( abs (( seq_id tseq) - ( seq_id (vseq . n)))) is summable by A43, SERIES_1: 17;

          then ( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) is convergent by SERIES_1:def 2;

          then ( Sum ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) = ( lim ( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n)))))) & ( lim ( Partial_Sums ( abs (( seq_id tseq) - ( seq_id (vseq . n)))))) <= e by A37, RSSPACE2: 5, SERIES_1:def 3;

          hence thesis by A14, A44, A43, SERIES_1: 17, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      ( abs ( seq_id tseq)) is summable

      proof

        set d = ( abs ( seq_id tseq));

        

         A45: for i be Nat holds 0 <= (( abs ( seq_id tseq)) . i)

        proof

          let i be Nat;

          (( abs ( seq_id tseq)) . i) = |.(( seq_id tseq) . i).| by SEQ_1: 12;

          hence thesis by COMPLEX1: 46;

        end;

        consider m be Nat such that

         A46: for n be Nat st n >= m holds ( abs (( seq_id tseq) - ( seq_id (vseq . n)))) is summable & ( Sum ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) < 1 by A12;

        set b = ( abs ( seq_id (vseq . m)));

        set a = ( abs (( seq_id tseq) - ( seq_id (vseq . m))));

        ( seq_id (vseq . m)) is absolutely_summable by Def1;

        then

         A47: ( abs ( seq_id (vseq . m))) is summable by SERIES_1:def 4;

        

         A48: for i be Nat holds (d . i) <= ((a + b) . i)

        proof

          let i be Nat;

          

           A49: (b . i) = |.(( seq_id (vseq . m)) . i).| & (d . i) = |.(( seq_id tseq) . i).| by SEQ_1: 12;

          (a . i) = |.((( seq_id tseq) - ( seq_id (vseq . m))) . i).| by SEQ_1: 12

          .= |.((( seq_id tseq) + ( - ( seq_id (vseq . m)))) . i).| by SEQ_1: 11

          .= |.((( seq_id tseq) . i) + (( - ( seq_id (vseq . m))) . i)).| by SEQ_1: 7

          .= |.((( seq_id tseq) . i) + ( - (( seq_id (vseq . m)) . i))).| by SEQ_1: 10

          .= |.((( seq_id tseq) . i) - (( seq_id (vseq . m)) . i)).|;

          then ((d . i) - (b . i)) <= (a . i) by A49, COMPLEX1: 59;

          then (((d . i) - (b . i)) + (b . i)) <= ((a . i) + (b . i)) by XREAL_1: 6;

          hence thesis by SEQ_1: 7;

        end;

        ( abs (( seq_id tseq) - ( seq_id (vseq . m)))) is summable by A46;

        then (a + b) is summable by A47, SERIES_1: 7;

        hence thesis by A45, A48, SERIES_1: 20;

      end;

      then

       A50: ( seq_id tseq) is absolutely_summable by SERIES_1:def 4;

      

       A51: tseq in the_set_of_RealSequences by FUNCT_2: 8;

      then

      reconsider tv = tseq as Point of l1_Space by A50, Def1;

      for e be Real st e > 0 holds ex m be Nat st for n be Nat st n >= m holds ||.((vseq . n) - tv).|| < e

      proof

        let e be Real;

        assume e > 0 ;

        then

        consider m be Nat such that

         A52: for n be Nat st n >= m holds ( abs (( seq_id tseq) - ( seq_id (vseq . n)))) is summable & ( Sum ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) < e by A12;

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

        take m;

        reconsider u = tseq as VECTOR of l1_Space by A50, A51, Def1;

        let n be Nat;

        assume n >= m;

        then

         A53: ( Sum ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) < e by A52;

        reconsider v = (vseq . n) as VECTOR of l1_Space ;

        ( seq_id (u - v)) = (u - v) by Th6;

        then ( Sum ( abs ( seq_id (u - v)))) = ( Sum ( abs (( seq_id tseq) - ( seq_id (vseq . n))))) by Th6;

        then

         A54: (the normF of l1_Space . (u - v)) < e by A53, Def2;

         ||.((vseq . n) - tv).|| = ||.( - (tv - (vseq . n))).|| by RLVECT_1: 33

        .= ||.(tv - (vseq . n)).|| by NORMSP_1: 2;

        hence ||.((vseq . n) - tv).|| < e by A54;

      end;

      hence thesis by NORMSP_1:def 6;

    end;