csspace3.miz



    begin

    definition

      :: CSSPACE3:def1

      func the_set_of_l1ComplexSequences -> Subset of Linear_Space_of_ComplexSequences means

      : Def1: for x be object holds x in it iff x in the_set_of_ComplexSequences & ( 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_ComplexSequences & P[x] from XBOOLE_0:sch 1;

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

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

        hence thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of Linear_Space_of_ComplexSequences ;

        assume that

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

         A3: for x be object holds x in X2 iff x in the_set_of_ComplexSequences & ( 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_ComplexSequences & ( 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_ComplexSequences & ( 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 :: CSSPACE3:1

    

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

    proof

      let c be Complex;

      let seq be Complex_Sequence;

      let rseq be Real_Sequence;

      assume that

       A1: seq is convergent and

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

      reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def 2;

      reconsider cseq = ( NAT --> c1) as Complex_Sequence;

      

       A3: for n be Nat holds (cseq . n) = c by ORDINAL1:def 12, FUNCOP_1: 7;

      then

       A4: cseq is convergent by COMSEQ_2: 9;

      then

      reconsider seq9 = (seq - cseq) as convergent Complex_Sequence by A1;

      (seq - cseq) is convergent by A1, A4;

      

      then

       A5: ( lim |.(seq - cseq).|) = |.( lim (seq - cseq)).| by SEQ_2: 27

      .= |.(( lim seq) - ( lim cseq)).| by A1, A4, COMSEQ_2: 26

      .= |.(( lim seq) - c).| by A3, COMSEQ_2: 10;

      now

        let i be Nat;

        

         A6: i in NAT by ORDINAL1:def 12;

        

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

        .= |.((seq . i) - (cseq . i)).| by FUNCOP_1: 7, A6

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

        .= |.((seq . i) + (( - cseq) . i)).| by VALUED_1: 8

        .= |.((seq - cseq) . i).| by VALUED_1: 1, A6

        .= ( |.(seq - cseq).| . i) by VALUED_1: 18;

      end;

      then

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

       |.seq9.| is convergent;

      hence thesis by A7, A5, FUNCT_2: 12;

    end;

    registration

      cluster the_set_of_l1ComplexSequences -> non empty;

      coherence

      proof

        ( seq_id CZeroseq ) is absolutely_summable

        proof

          reconsider cseq = ( seq_id CZeroseq ) as Complex_Sequence;

          for n be Nat holds (cseq . n) = 0c by CSSPACE: 4;

          hence thesis by COMSEQ_3: 51;

        end;

        hence thesis by Def1;

      end;

    end

    registration

      cluster the_set_of_l1ComplexSequences -> linearly-closed;

      coherence

      proof

        set W = the_set_of_l1ComplexSequences ;

        

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

        proof

          let v,u be VECTOR of Linear_Space_of_ComplexSequences such that

           A2: v in W and

           A3: u in W;

          ( seq_id (v + u)) is absolutely_summable

          proof

            set r = |.( seq_id (v + u)).|;

            set q = |.( seq_id u).|;

            set p = |.( 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 VALUED_1: 18;

              hence thesis by COMPLEX1: 46;

            end;

            

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

            proof

              let n be Nat;

              

               A6: n in NAT by ORDINAL1:def 12;

              

               A7: ( |.(( seq_id v) . n).| + |.(( seq_id u) . n).|) = (( |.( seq_id v).| . n) + |.(( seq_id u) . n).|) by VALUED_1: 18

              .= (( |.( seq_id v).| . n) + ( |.( seq_id u).| . n)) by VALUED_1: 18

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

              (r . n) = |.(( seq_id (v + u)) . n).| by VALUED_1: 18

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

              .= |.((( seq_id v) . n) + (( seq_id u) . n)).| by VALUED_1: 1, A6;

              hence thesis by A7, COMPLEX1: 56;

            end;

            ( seq_id u) is absolutely_summable by A3, Def1;

            then

             A8: q is summable by COMSEQ_3:def 9;

            ( seq_id v) is absolutely_summable by A2, Def1;

            then p is summable by COMSEQ_3:def 9;

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

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

            hence thesis by COMSEQ_3:def 9;

          end;

          hence thesis by Def1;

        end;

        for a be Complex, v be VECTOR of Linear_Space_of_ComplexSequences st v in W holds (a * v) in W

        proof

          let a be Complex;

          let v be VECTOR of Linear_Space_of_ComplexSequences such that

           A9: v in W;

          ( seq_id (a * v)) is absolutely_summable

          proof

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

            set q1 = |.( seq_id (a * v)).|;

            

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

            proof

              let n be Nat;

              (q1 . n) = |.(( seq_id (a * v)) . n).| by VALUED_1: 18;

              hence thesis by COMPLEX1: 46;

            end;

            

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

            proof

              let n be Nat;

              (q1 . n) = |.(( seq_id (a * v)) . n).| by VALUED_1: 18

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

              .= ( |.(a (#) ( seq_id v)).| . n) by VALUED_1: 18;

              hence thesis by COMSEQ_1: 50;

            end;

            ( seq_id v) is absolutely_summable by A9, Def1;

            then |.( seq_id v).| is summable by COMSEQ_3:def 9;

            then r1 is summable by SERIES_1: 10;

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

            hence thesis by COMSEQ_3:def 9;

          end;

          hence thesis by Def1;

        end;

        hence thesis by A1, CLVECT_1:def 7;

      end;

    end

    

     Lm1: CLSStruct (# the_set_of_l1ComplexSequences , ( Zero_ ( the_set_of_l1ComplexSequences , Linear_Space_of_ComplexSequences )), ( Add_ ( the_set_of_l1ComplexSequences , Linear_Space_of_ComplexSequences )), ( Mult_ ( the_set_of_l1ComplexSequences , Linear_Space_of_ComplexSequences )) #) is Subspace of Linear_Space_of_ComplexSequences by CSSPACE: 11;

    registration

      cluster CLSStruct (# the_set_of_l1ComplexSequences , ( Zero_ ( the_set_of_l1ComplexSequences , Linear_Space_of_ComplexSequences )), ( Add_ ( the_set_of_l1ComplexSequences , Linear_Space_of_ComplexSequences )), ( Mult_ ( the_set_of_l1ComplexSequences , Linear_Space_of_ComplexSequences )) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by CSSPACE: 11;

    end

    definition

      :: CSSPACE3:def2

      func cl_norm -> Function of the_set_of_l1ComplexSequences , REAL means

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

      existence

      proof

        deffunc F( object) = ( Sum |.( seq_id $1).|);

        

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

        ex f be Function of the_set_of_l1ComplexSequences , REAL st for x be object st x in the_set_of_l1ComplexSequences 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_l1ComplexSequences , REAL such that

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

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

        

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

        proof

          let z be object such that

           A5: z in the_set_of_l1ComplexSequences ;

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

          hence thesis by A3, A5;

        end;

        ( dom NORM1) = the_set_of_l1ComplexSequences & ( dom NORM2) = the_set_of_l1ComplexSequences 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 [: COMPLEX , X:], X, N be Function of X, REAL ;

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

      coherence ;

    end

    theorem :: CSSPACE3:2

    for l be CNORMSTR st the CLSStruct of l is ComplexLinearSpace holds l is ComplexLinearSpace by CSSPACE: 79;

    theorem :: CSSPACE3:3

    

     Th3: for cseq be Complex_Sequence st (for n be Nat holds (cseq . n) = 0c ) holds cseq is absolutely_summable & ( Sum |.cseq.|) = 0

    proof

      let cseq be Complex_Sequence such that

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

      

       A2: for n be Nat holds ( |.cseq.| . n) = 0

      proof

        let n be Nat;

        (cseq . n) = 0c by A1;

        hence thesis by COMPLEX1: 44, VALUED_1: 18;

      end;

      

       A3: for m be Nat holds (( Partial_Sums |.cseq.|) . m) = 0

      proof

        defpred P[ Nat] means ( |.cseq.| . $1) = (( Partial_Sums |.cseq.|) . $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: ( |.cseq.| . k) = (( Partial_Sums |.cseq.|) . k);

          

          thus ( |.cseq.| . (k + 1)) = ( 0 + ( |.cseq.| . (k + 1)))

          .= (( |.cseq.| . k) + ( |.cseq.| . (k + 1))) by A2

          .= (( Partial_Sums |.cseq.|) . (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 |.cseq.|) . m) = ( |.cseq.| . 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 |.cseq.|) . 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 |.cseq.|) . m) - 0 ).| = |.( 0 - 0 ).| by A3

        .= 0 by ABSVALUE:def 1;

        hence thesis by A8;

      end;

      then

       A9: ( Partial_Sums |.cseq.|) is convergent by SEQ_2:def 6;

      then

       A10: |.cseq.| is summable by SERIES_1:def 2;

      ( lim ( Partial_Sums |.cseq.|)) = 0 by A7, A9, SEQ_2:def 7;

      hence thesis by A10, COMSEQ_3:def 9, SERIES_1:def 3;

    end;

    

     Lm2: CLSStruct (# the_set_of_l1ComplexSequences , ( Zero_ ( the_set_of_l1ComplexSequences , Linear_Space_of_ComplexSequences )), ( Add_ ( the_set_of_l1ComplexSequences , Linear_Space_of_ComplexSequences )), ( Mult_ ( the_set_of_l1ComplexSequences , Linear_Space_of_ComplexSequences )) #) is ComplexLinearSpace;

    definition

      :: CSSPACE3:def3

      func Complex_l1_Space -> non empty CNORMSTR equals CNORMSTR (# the_set_of_l1ComplexSequences , ( Zero_ ( the_set_of_l1ComplexSequences , Linear_Space_of_ComplexSequences )), ( Add_ ( the_set_of_l1ComplexSequences , Linear_Space_of_ComplexSequences )), ( Mult_ ( the_set_of_l1ComplexSequences , Linear_Space_of_ComplexSequences )), cl_norm #);

      coherence ;

    end

    ::$Canceled

    theorem :: CSSPACE3:5

    

     Th4: Complex_l1_Space is ComplexLinearSpace by Lm2, CSSPACE: 79;

    begin

    theorem :: CSSPACE3:6

    

     Th5: the carrier of Complex_l1_Space = the_set_of_l1ComplexSequences & (for x be set holds x is VECTOR of Complex_l1_Space iff x is Complex_Sequence & ( seq_id x) is absolutely_summable) & ( 0. Complex_l1_Space ) = CZeroseq & (for u be VECTOR of Complex_l1_Space holds u = ( seq_id u)) & (for u,v be VECTOR of Complex_l1_Space holds (u + v) = (( seq_id u) + ( seq_id v))) & (for p be Complex holds for u be VECTOR of Complex_l1_Space holds (p * u) = (p (#) ( seq_id u))) & (for u be VECTOR of Complex_l1_Space holds ( - u) = ( - ( seq_id u)) & ( seq_id ( - u)) = ( - ( seq_id u))) & (for u,v be VECTOR of Complex_l1_Space holds (u - v) = (( seq_id u) - ( seq_id v))) & (for v be VECTOR of Complex_l1_Space holds ( seq_id v) is absolutely_summable) & for v be VECTOR of Complex_l1_Space holds ||.v.|| = ( Sum |.( seq_id v).|)

    proof

      set l1 = Complex_l1_Space ;

      

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

      proof

        let x be set;

        x in the_set_of_ComplexSequences iff x is Complex_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_ComplexSequences by Lm1, CLVECT_1: 29;

        set L1 = Linear_Space_of_ComplexSequences ;

        set W = the_set_of_l1ComplexSequences ;

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

        then

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

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

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

        hence thesis by CSSPACE: 2;

      end;

      

       A4: for p be Complex holds for u be VECTOR of l1 holds (p * u) = (p (#) ( seq_id u))

      proof

        let p be Complex;

        let u be VECTOR of l1;

        reconsider u1 = u as VECTOR of Linear_Space_of_ComplexSequences by Lm1, CLVECT_1: 29;

        set L1 = Linear_Space_of_ComplexSequences ;

        set W = the_set_of_l1ComplexSequences ;

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

        then

         A5: ( dom (the Mult of Linear_Space_of_ComplexSequences | [: COMPLEX , W:])) = [: COMPLEX , W:] by RELAT_1: 62, ZFMISC_1: 96;

        reconsider p as Element of COMPLEX by XCMPLX_0:def 2;

        (p * u) = (the Mult of l1 . [p, u]) by CLVECT_1:def 1

        .= ((the Mult of Linear_Space_of_ComplexSequences | [: COMPLEX , W:]) . [p, u]) by CSSPACE:def 9

        .= (the Mult of Linear_Space_of_ComplexSequences . [p, u]) by A5, FUNCT_1: 47

        .= (p * u1) by CLVECT_1:def 1;

        hence thesis by CSSPACE: 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_ComplexSequences by Lm1, CLVECT_1: 29;

        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) = (( - 1r ) * u) by Th4, CLVECT_1: 3

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

        .= ( - ( seq_id u)) by COMSEQ_1: 11;

        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;

      end;

      

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

      ( 0. l1) = ( 0. Linear_Space_of_ComplexSequences ) by CSSPACE:def 10

      .= CZeroseq ;

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

    end;

    theorem :: CSSPACE3:7

    

     Th6: for x,y be Point of Complex_l1_Space , p be Complex holds ( ||.x.|| = 0 iff x = ( 0. Complex_l1_Space )) & 0 <= ||.x.|| & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) & ||.(p * x).|| = ( |.p.| * ||.x.||)

    proof

      let x,y be Point of Complex_l1_Space ;

      let p be Complex;

      

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

      proof

        let n be Nat;

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

        hence thesis by VALUED_1: 18;

      end;

       A2:

      now

        let n be Nat;

        ( |.( seq_id (x + y)).| . n) = |.(( seq_id (x + y)) . n).| by VALUED_1: 18;

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

      end;

      

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

      proof

        let n be Nat;

        

         A4: n in NAT by ORDINAL1:def 12;

        ( |.( seq_id (x + y)).| . n) = ( |.( seq_id (( seq_id x) + ( seq_id y))).| . n) by Th5

        .= |.((( seq_id x) + ( seq_id y)) . n).| by VALUED_1: 18

        .= |.((( seq_id x) . n) + (( seq_id y) . n)).| by VALUED_1: 1, A4;

        hence thesis;

      end;

      

       A5: for n be Nat holds ( |.( seq_id (x + y)).| . n) <= (( |.( seq_id x).| . n) + ( |.( 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 ( |.( seq_id (x + y)).| . n) <= ( |.(( seq_id x) . n).| + |.(( seq_id y) . n).|) by A3;

        then ( |.( seq_id (x + y)).| . n) <= (( |.( seq_id x).| . n) + |.(( seq_id y) . n).|) by VALUED_1: 18;

        hence thesis by VALUED_1: 18;

      end;

      

       A6: for n be Nat holds ( |.( seq_id (x + y)).| . n) <= (( |.( seq_id x).| + |.( seq_id y).|) . n)

      proof

        let n be Nat;

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

        hence thesis by A5;

      end;

      ( seq_id y) is absolutely_summable by Def1;

      then

       A7: |.( seq_id y).| is summable by COMSEQ_3:def 9;

      ( seq_id x) is absolutely_summable by Def1;

      then |.( seq_id x).| is summable by COMSEQ_3:def 9;

      then ( |.( seq_id x).| + |.( seq_id y).|) is summable by A7, SERIES_1: 7;

      then

       A8: ( Sum |.( seq_id (x + y)).|) <= ( Sum ( |.( seq_id x).| + |.( seq_id y).|)) by A6, A2, SERIES_1: 20;

       A9:

      now

        assume x = ( 0. Complex_l1_Space );

        then

         A10: for n be Nat holds (( seq_id x) . n) = 0 by Th5, CSSPACE: 4;

        

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

        .= 0 by A10, Th3;

      end;

      

       A11: ( Sum |.( seq_id (x + y)).|) = ||.(x + y).|| by Th5;

       A12:

      now

        

         A13: x in the_set_of_ComplexSequences by Def1;

        assume

         A14: ||.x.|| = 0 ;

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

        then for n be Nat holds 0 = (( seq_id x) . n) by A14, CSSPACE2: 13;

        hence x = ( 0. Complex_l1_Space ) by A13, Th5, CSSPACE: 5;

      end;

      

       A15: ||.x.|| = ( Sum |.( seq_id x).|) & ||.y.|| = ( Sum |.( seq_id y).|) by Th5;

      

       A16: for n be Nat holds ( |.(p (#) ( seq_id x)).| . n) = ( |.p.| * ( |.( seq_id x).| . n))

      proof

        let n be Nat;

        reconsider p as Element of COMPLEX by XCMPLX_0:def 2;

        ( |.(p (#) ( seq_id x)).| . n) = |.((p (#) ( seq_id x)) . n).| by VALUED_1: 18

        .= |.(p * (( seq_id x) . n)).| by VALUED_1: 6

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

        .= ( |.p.| * ( |.( seq_id x).| . n)) by VALUED_1: 18;

        hence thesis;

      end;

      ( seq_id x) is absolutely_summable by Def1;

      then

       A17: |.( seq_id x).| is summable by COMSEQ_3:def 9;

      ( seq_id x) is absolutely_summable by Def1;

      then

       A18: |.( seq_id x).| is summable by COMSEQ_3:def 9;

       ||.(p * x).|| = ( Sum |.( seq_id (p * x)).|) by Th5

      .= ( Sum |.( seq_id (p (#) ( seq_id x))).|) by Th5

      .= ( Sum ( |.p.| (#) |.( seq_id x).|)) by A16, SEQ_1: 9

      .= ( |.p.| * ( Sum |.( seq_id x).|)) by A17, SERIES_1: 10

      .= ( |.p.| * ||.x.||) by Th5;

      hence thesis by A12, A9, A1, A18, A15, A11, A7, A8, SERIES_1: 7, SERIES_1: 18;

    end;

    registration

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

      coherence by Lm2, Th6, CLVECT_1:def 13, CSSPACE: 79;

    end

    

     Lm3: for c be Complex, seq be Complex_Sequence, 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 Complex;

      let seq be Complex_Sequence;

      let seq1 be Real_Sequence;

      assume that

       A1: seq is convergent and

       A2: seq1 is convergent;

      reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def 2;

      reconsider cseq = ( NAT --> c1) as Complex_Sequence;

      

       A3: for n be Nat holds (cseq . n) = c by ORDINAL1:def 12, FUNCOP_1: 7;

      

      then

       A4: ( lim cseq) = c by COMSEQ_2: 10

      .= (cseq . 0 ) by FUNCOP_1: 7;

      

       A5: cseq is convergent by A3, COMSEQ_2: 9;

      then (seq - cseq) is convergent by A1;

      

      then

       A6: ( lim |.(seq - cseq).|) = |.( lim (seq - cseq)).| by SEQ_2: 27

      .= |.(( lim seq) - (cseq . 0 )).| by A1, A4, A5, COMSEQ_2: 26

      .= |.(( lim seq) - c).| by FUNCOP_1: 7;

      let rseq be Real_Sequence such that

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

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

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

        .= ( |.((seq . i) + (( - cseq) . i)).| + (seq1 . i)) by VALUED_1: 8

        .= ( |.((seq - cseq) . i).| + (seq1 . i)) by VALUED_1: 1

        .= (( |.(seq - cseq).| . i) + (seq1 . i)) by VALUED_1: 18

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

      end;

      then

       A8: rseq = ( |.(seq - cseq).| + seq1) by FUNCT_2: 63;

      reconsider seq1 = (seq - cseq) as convergent Complex_Sequence by A1, A5;

       |.seq1.| is convergent;

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

    end;

    definition

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

      :: CSSPACE3:def4

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

      coherence ;

    end

    definition

      let CNRM be non empty CNORMSTR;

      let seqt be sequence of CNRM;

      :: CSSPACE3: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 CNRM be non empty CNORMSTR;

      let seq be sequence of CNRM;

      synonym seq is Cauchy_sequence_by_Norm for seq is CCauchy;

    end

    reserve NRM for non empty ComplexNormSpace;

    reserve seq for sequence of NRM;

    theorem :: CSSPACE3:8

    

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

      thus (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) implies seq is Cauchy_sequence_by_Norm

      proof

        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;

    end;

    theorem :: CSSPACE3:9

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

    proof

      let vseq be sequence of Complex_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 Complex_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 COMPLEX & P[x, y]

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Element of NAT ;

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

        consider rseqi be Complex_Sequence such that

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

        take ( lim rseqi);

        thus ( lim rseqi) in COMPLEX by XCMPLX_0:def 2;

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

            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 VALUED_1: 18;

              end;

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

              then |.( seq_id ((vseq . m) - (vseq . k))).| is summable by COMSEQ_3:def 9;

              then

               A8: ( |.( 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 Th5

              .= (( seq_id (vseq . m)) + ( - ( seq_id (vseq . k))));

              

              then (( seq_id ((vseq . m) - (vseq . k))) . i) = ((( seq_id (vseq . m)) . i) + (( - ( seq_id (vseq . k))) . i)) by VALUED_1: 1

              .= ((( seq_id (vseq . m)) . i) + ( - (( seq_id (vseq . k)) . i))) by VALUED_1: 8

              .= ((( 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)).| = ( |.( seq_id ((vseq . m) - (vseq . k))).| . i) by VALUED_1: 18;

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

              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 COMSEQ_3: 46;

        hence thesis by A3;

      end;

      consider f be sequence of COMPLEX 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 Complex_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 Complex_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 Complex_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 |.(( seq_id tseq) - ( seq_id (vseq . n))).| is summable & ( Sum |.(( seq_id tseq) - ( seq_id (vseq . n))).|) < e

      proof

        let e1 be Real such that

         A13: e1 > 0 ;

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

        

         A16: for m,n be Nat st n >= k & m >= k holds ( |.( seq_id ((vseq . n) - (vseq . m))).| is summable & ( Sum |.( seq_id ((vseq . n) - (vseq . m))).|) < e & for i be Nat holds 0 <= ( |.( 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 Complex_l1_Space . ((vseq . n) - (vseq . m))) < e;

          

           A18: for i be Nat holds 0 <= ( |.( 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 VALUED_1: 18;

          end;

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

          hence thesis by A17, A18, Def2, COMSEQ_3:def 9;

        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 |.( seq_id ((vseq . m) - (vseq . n))).|) . i)) holds rseq is convergent & ( lim rseq) = (( Partial_Sums |.(( 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 |.( seq_id ((vseq . m) - (vseq . n))).|) . $1) holds rseq is convergent & ( lim rseq) = (( Partial_Sums |.(( 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 Th5;

            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 |.( seq_id ((vseq . m) - (vseq . n))).|) . i)) holds rseq is convergent & ( lim rseq) = (( Partial_Sums |.(( seq_id tseq) - ( seq_id (vseq . n))).|) . i);

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

            proof

              deffunc F( Nat) = (( Partial_Sums |.( 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 Complex_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 |.( seq_id ((vseq . m) - (vseq . n))).|) . (i + 1));

               A27:

              now

                let m be Nat;

                

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

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

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

                .= (( |.(( 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 VALUED_1: 18

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

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

                .= ( |.((( 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 VALUED_1: 8

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

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

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

              .= (( Partial_Sums |.(( 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 |.( seq_id ((vseq . m) - (vseq . n))).|) . 0 );

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

            proof

              consider rseq0 be Complex_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 |.( seq_id ((vseq . m) - (vseq . n))).|) . 0 ) by A30

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

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

                .= |.((( seq_id (vseq . m)) + ( - ( seq_id (vseq . n)))) . 0 ).| by VALUED_1: 18

                .= |.((( seq_id (vseq . m)) . 0 ) + (( - ( seq_id (vseq . n))) . 0 )).| by VALUED_1: 1

                .= |.((( seq_id (vseq . m)) . 0 ) + ( - (( seq_id (vseq . n)) . 0 ))).| by VALUED_1: 8

                .= |.((( 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 VALUED_1: 8

              .= |.((tseq - ( seq_id (vseq . n))) . 0 ).| by VALUED_1: 1

              .= ( |.(( seq_id tseq) - ( seq_id (vseq . n))).| . 0 ) by VALUED_1: 18

              .= (( Partial_Sums |.(( 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 |.(( seq_id tseq) - ( seq_id (vseq . n))).| is summable & ( Sum |.(( 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 |.(( seq_id tseq) - ( seq_id (vseq . n))).|) . i) <= e

          proof

            let i be Nat such that 0 <= i;

            deffunc F( Nat) = (( Partial_Sums |.( 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 |.( seq_id ((vseq . m) - (vseq . n))).|) . i) by A38;

              assume

               A41: m >= k;

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

              then

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

              ( Sum |.( 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 |.(( 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 |.(( seq_id tseq) - ( seq_id (vseq . n))).|) . i) <= e by A37, NAT_1: 2;

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

          end;

          then

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

          

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

          proof

            let i be Nat;

            ( |.(( seq_id tseq) - ( seq_id (vseq . n))).| . i) = |.((( seq_id tseq) - ( seq_id (vseq . n))) . i).| by VALUED_1: 18;

            hence thesis by COMPLEX1: 46;

          end;

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

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

          then ( Sum |.(( seq_id tseq) - ( seq_id (vseq . n))).|) = ( lim ( Partial_Sums |.(( seq_id tseq) - ( seq_id (vseq . n))).|)) & ( lim ( Partial_Sums |.(( 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;

       |.( seq_id tseq).| is summable

      proof

        set d = |.( seq_id tseq).|;

        

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

        proof

          let i be Nat;

          ( |.( seq_id tseq).| . i) = |.(( seq_id tseq) . i).| by VALUED_1: 18;

          hence thesis by COMPLEX1: 46;

        end;

        reconsider jj = 1 as Real;

        consider m be Nat such that

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

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

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

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

        then

         A47: |.( seq_id (vseq . m)).| is summable by COMSEQ_3:def 9;

        

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

        proof

          let i be Nat;

          

           A49: i in NAT by ORDINAL1:def 12;

          

           A50: (b . i) = |.(( seq_id (vseq . m)) . i).| & (d . i) = |.(( seq_id tseq) . i).| by VALUED_1: 18;

          (a . i) = |.((( seq_id tseq) + ( - ( seq_id (vseq . m)))) . i).| by VALUED_1: 18

          .= |.((( seq_id tseq) . i) + (( - ( seq_id (vseq . m))) . i)).| by VALUED_1: 1, A49

          .= |.((( seq_id tseq) . i) + ( - (( seq_id (vseq . m)) . i))).| by VALUED_1: 8

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

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

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

          hence thesis by SEQ_1: 7;

        end;

         |.(( 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

       A51: ( seq_id tseq) is absolutely_summable by COMSEQ_3:def 9;

      

       A52: tseq in the_set_of_ComplexSequences by FUNCT_2: 8;

      then

      reconsider tv = tseq as Point of Complex_l1_Space by A51, 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

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

        now

          reconsider u = tseq as VECTOR of Complex_l1_Space by A51, A52, Def1;

          let n be Nat;

          assume n >= m;

          then

           A54: ( Sum |.(( seq_id tseq) - ( seq_id (vseq . n))).|) < e by A53;

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

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

          then ( Sum |.( seq_id (u - v)).|) = ( Sum |.(( seq_id tseq) - ( seq_id (vseq . n))).|) by Th5;

          then

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

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

          .= ||.(tv - (vseq . n)).|| by CLVECT_1: 103;

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

        end;

        hence thesis;

      end;

      hence thesis by CLVECT_1:def 15;

    end;