csspace4.miz



    begin

    

     Lm1: for rseq be Real_Sequence holds for K be Real st (for n be Nat holds (rseq . n) <= K) holds ( upper_bound ( rng rseq)) <= K

    proof

      let rseq be Real_Sequence;

      let K be Real such that

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

      now

        let s be Real;

        assume s in ( rng rseq);

        then ex n be object st n in NAT & (rseq . n) = s by FUNCT_2: 11;

        hence s <= K by A1;

      end;

      hence thesis by SEQ_4: 45;

    end;

    

     Lm2: for rseq be Real_Sequence st rseq is bounded holds for n be Nat holds (rseq . n) <= ( upper_bound ( rng rseq))

    proof

      let rseq be Real_Sequence;

      assume rseq is bounded;

      then ( rng rseq) is real-bounded by MEASURE6: 39;

      then

       A1: ( rng rseq) is bounded_above;

      let n be Nat;

      

       A2: n in NAT by ORDINAL1:def 12;

       NAT = ( dom rseq) by FUNCT_2:def 1;

      then (rseq . n) in ( rng rseq) by FUNCT_1: 3, A2;

      hence thesis by A1, SEQ_4:def 1;

    end;

    definition

      :: CSSPACE4:def1

      func the_set_of_BoundedComplexSequences -> 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 bounded;

      existence

      proof

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

        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 bounded and

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

        thus X1 c= X2

        proof

          let x be object;

          assume x in X1;

          then x in the_set_of_ComplexSequences & ( seq_id x) is bounded by A2;

          hence thesis by A3;

        end;

        let x be object;

        assume x in X2;

        then x in the_set_of_ComplexSequences & ( seq_id x) is bounded by A3;

        hence thesis by A2;

      end;

    end

    

     Lm3: for seq1,seq2 be Complex_Sequence st seq1 is bounded & seq2 is bounded holds (seq1 + seq2) is bounded

    proof

      let seq1,seq2 be Complex_Sequence;

      assume that

       A1: seq1 is bounded and

       A2: seq2 is bounded;

      consider r2 be Real such that 0 < r2 and

       A3: for n be Nat holds |.(seq2 . n).| < r2 by A2, COMSEQ_2: 8;

      consider r1 be Real such that 0 < r1 and

       A4: for n be Nat holds |.(seq1 . n).| < r1 by A1, COMSEQ_2: 8;

      for n be Nat holds |.((seq1 + seq2) . n).| < (r1 + r2)

      proof

        let n be Nat;

        

         A5: n in NAT by ORDINAL1:def 12;

         |.((seq1 + seq2) . n).| = |.((seq1 . n) + (seq2 . n)).| by VALUED_1: 1, A5;

        then

         A6: |.((seq1 + seq2) . n).| <= ( |.(seq1 . n).| + |.(seq2 . n).|) by COMPLEX1: 56;

         |.(seq1 . n).| < r1 by A4;

        then ( |.(seq1 . n).| + |.(seq2 . n).|) < (r1 + r2) by A3, XREAL_1: 8;

        hence thesis by A6, XXREAL_0: 2;

      end;

      hence thesis by COMSEQ_2:def 4;

    end;

    reconsider jj = 1 as Real;

    

     Lm4: for c be Complex, seq be Complex_Sequence st seq is bounded holds (c (#) seq) is bounded

    proof

      let c be Complex;

      let seq be Complex_Sequence;

      assume seq is bounded;

      then

      consider r be Real such that 0 < r and

       A1: for n be Nat holds |.(seq . n).| < r by COMSEQ_2: 8;

      ex r1 be Real st for n be Nat holds |.((c (#) seq) . n).| < r1

      proof

        now

          per cases ;

            case

             A2: c = 0c ;

            take r1 = 1;

            for n be Nat holds |.((c (#) seq) . n).| < jj

            proof

              let n be Nat;

              ((c (#) seq) . n) = (c * (seq . n)) by VALUED_1: 6

              .= 0 by A2;

              hence thesis by COMPLEX1: 44;

            end;

            hence thesis;

          end;

            case

             A3: c <> 0c ;

            take r1 = ( |.c.| * r);

            for n be Nat holds |.((c (#) seq) . n).| < ( |.c.| * r)

            proof

              let n be Nat;

              

               A4: |.((c (#) seq) . n).| = |.(c * (seq . n)).| by VALUED_1: 6

              .= ( |.c.| * |.(seq . n).|) by COMPLEX1: 65;

               |.c.| > 0 by A3, COMPLEX1: 47;

              hence thesis by A1, A4, XREAL_1: 68;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis by COMSEQ_2:def 4;

    end;

    registration

      cluster the_set_of_BoundedComplexSequences -> non empty;

      coherence

      proof

        ( seq_id CZeroseq ) is bounded

        proof

          reconsider seq = ( seq_id CZeroseq ) as Complex_Sequence;

          for n be Nat holds |.(seq . n).| < jj by COMPLEX1: 44;

          hence thesis by COMSEQ_2: 8;

        end;

        hence thesis by Def1;

      end;

      cluster the_set_of_BoundedComplexSequences -> linearly-closed;

      coherence

      proof

        set W = the_set_of_BoundedComplexSequences ;

        

         A1: for c be Complex, v be VECTOR of Linear_Space_of_ComplexSequences st v in W holds (c * v) in W

        proof

          let c be Complex;

          let v be VECTOR of Linear_Space_of_ComplexSequences ;

          assume v in W;

          then

           A2: ( seq_id v) is bounded by Def1;

          ( seq_id (c * v)) = ( seq_id (c (#) ( seq_id v))) by CSSPACE: 3

          .= (c (#) ( seq_id v));

          then ( seq_id (c * v)) is bounded by A2, Lm4;

          hence thesis by Def1;

        end;

        for v,u be VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_BoundedComplexSequences & u in the_set_of_BoundedComplexSequences holds (v + u) in the_set_of_BoundedComplexSequences

        proof

          let v,u be VECTOR of Linear_Space_of_ComplexSequences ;

          assume v in W & u in W;

          then

           A3: ( seq_id v) is bounded & ( seq_id u) is bounded by Def1;

          ( seq_id (v + u)) = ( seq_id (( seq_id v) + ( seq_id u))) by CSSPACE: 2

          .= (( seq_id v) + ( seq_id u));

          then ( seq_id (v + u)) is bounded by A3, Lm3;

          hence thesis by Def1;

        end;

        hence thesis by A1, CLVECT_1:def 7;

      end;

    end

    

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

    registration

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

      coherence by CSSPACE: 11;

    end

    

     Lm6: CLSStruct (# the_set_of_BoundedComplexSequences , ( Zero_ ( the_set_of_BoundedComplexSequences , Linear_Space_of_ComplexSequences )), ( Add_ ( the_set_of_BoundedComplexSequences , Linear_Space_of_ComplexSequences )), ( Mult_ ( the_set_of_BoundedComplexSequences , Linear_Space_of_ComplexSequences )) #) is Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

    definition

      :: CSSPACE4:def2

      func Complex_linfty_norm -> Function of the_set_of_BoundedComplexSequences , REAL means

      : Def2: for x be object st x in the_set_of_BoundedComplexSequences holds (it . x) = ( upper_bound ( rng |.( seq_id x).|));

      existence

      proof

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

        

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

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

         A2: for x be object st x in the_set_of_BoundedComplexSequences holds (NORM1 . x) = ( upper_bound ( rng |.( seq_id x).|)) and

         A3: for x be object st x in the_set_of_BoundedComplexSequences holds (NORM2 . x) = ( upper_bound ( rng |.( seq_id x).|));

        

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

        proof

          let z be object such that

           A5: z in the_set_of_BoundedComplexSequences ;

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

          hence thesis by A3, A5;

        end;

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

        hence thesis by A4, FUNCT_1: 2;

      end;

    end

    

     Lm7: for seq be Complex_Sequence st (for n be Nat holds (seq . n) = 0c ) holds seq is bounded & ( upper_bound ( rng |.seq.|)) = 0

    proof

      let seq be Complex_Sequence such that

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

      for n be Nat holds |.(seq . n).| < jj by A1, COMPLEX1: 44;

      hence seq is bounded by COMSEQ_2:def 4;

      ( rng |.seq.|) c= { 0 }

      proof

        let y be object;

        assume y in ( rng |.seq.|);

        then

        consider n be object such that

         A2: n in NAT and

         A3: ( |.seq.| . n) = y by FUNCT_2: 11;

        reconsider n as Nat by A2;

        ( |.seq.| . n) = |.(seq . n).| by VALUED_1: 18

        .= |. 0c .| by A1;

        hence thesis by A3, COMPLEX1: 44, TARSKI:def 1;

      end;

      then ( rng |.seq.|) = { 0 } by ZFMISC_1: 33;

      hence thesis by SEQ_4: 9;

    end;

    

     Lm8: for seq be Complex_Sequence st seq is bounded holds |.seq.| is bounded

    proof

      let seq be Complex_Sequence;

      

       A1: 0 <= |.(seq . 0 ).| by COMPLEX1: 46;

      assume seq is bounded;

      then

      consider r be Real such that

       A2: for n be Nat holds |.(seq . n).| < r by COMSEQ_2:def 4;

      

       A3: for n be Nat holds |.( |.seq.| . n).| < r

      proof

        let n be Nat;

        ( |.seq.| . n) = |.(seq . n).| by VALUED_1: 18;

        hence thesis by A2;

      end;

       |.(seq . 0 ).| < r by A2;

      hence thesis by A1, A3, SEQ_2: 3;

    end;

    

     Lm9: for seq be Complex_Sequence st |.seq.| is bounded holds seq is bounded

    proof

      let seq be Complex_Sequence;

      assume |.seq.| is bounded;

      then

      consider r be Real such that 0 < r and

       A1: for n be Nat holds |.( |.seq.| . n).| < r by SEQ_2: 3;

      reconsider r as Real;

      for n be Nat holds |.(seq . n).| < r

      proof

        let n be Nat;

        ( |.seq.| . n) = |.(seq . n).| by VALUED_1: 18;

        then |.( |.seq.| . n).| = |.(seq . n).|;

        hence thesis by A1;

      end;

      hence thesis by COMSEQ_2:def 4;

    end;

    

     Lm10: for seq be Complex_Sequence st seq is bounded & ( upper_bound ( rng |.seq.|)) = 0 holds for n be Nat holds (seq . n) = 0c

    proof

      let seq be Complex_Sequence such that

       A1: seq is bounded and

       A2: ( upper_bound ( rng |.seq.|)) = 0 ;

      let n be Nat;

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

      then

       A3: 0 <= ( |.seq.| . n) by VALUED_1: 18;

       |.seq.| is bounded by A1, Lm8;

      then ( |.seq.| . n) = 0 by A2, A3, Lm2;

      then |.(seq . n).| = 0 by VALUED_1: 18;

      hence thesis by COMPLEX1: 45;

    end;

    theorem :: CSSPACE4:1

    for seq be Complex_Sequence holds seq is bounded & ( upper_bound ( rng |.seq.|)) = 0 iff for n be Nat holds (seq . n) = 0c by Lm7, Lm10;

    registration

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

      coherence by Lm6, CSSPACE3: 2;

    end

    definition

      :: CSSPACE4:def3

      func Complex_linfty_Space -> non empty CNORMSTR equals CNORMSTR (# the_set_of_BoundedComplexSequences , ( Zero_ ( the_set_of_BoundedComplexSequences , Linear_Space_of_ComplexSequences )), ( Add_ ( the_set_of_BoundedComplexSequences , Linear_Space_of_ComplexSequences )), ( Mult_ ( the_set_of_BoundedComplexSequences , Linear_Space_of_ComplexSequences )), Complex_linfty_norm #);

      coherence ;

    end

    theorem :: CSSPACE4:2

    

     Th2: the carrier of Complex_linfty_Space = the_set_of_BoundedComplexSequences & (for x be set holds x is VECTOR of Complex_linfty_Space iff x is Complex_Sequence & ( seq_id x) is bounded) & ( 0. Complex_linfty_Space ) = CZeroseq & (for u be VECTOR of Complex_linfty_Space holds u = ( seq_id u)) & (for u,v be VECTOR of Complex_linfty_Space holds (u + v) = (( seq_id u) + ( seq_id v))) & (for c be Complex, u be VECTOR of Complex_linfty_Space holds (c * u) = (c (#) ( seq_id u))) & (for u be VECTOR of Complex_linfty_Space holds ( - u) = ( - ( seq_id u)) & ( seq_id ( - u)) = ( - ( seq_id u))) & (for u,v be VECTOR of Complex_linfty_Space holds (u - v) = (( seq_id u) - ( seq_id v))) & (for v be VECTOR of Complex_linfty_Space holds ( seq_id v) is bounded) & for v be VECTOR of Complex_linfty_Space holds ||.v.|| = ( upper_bound ( rng |.( seq_id v).|))

    proof

      set l1 = Complex_linfty_Space ;

      

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

      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 Lm5, CLVECT_1: 29;

        set L1 = Linear_Space_of_ComplexSequences ;

        set W = the_set_of_BoundedComplexSequences ;

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

        (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 c be Complex, u be VECTOR of l1 holds (c * u) = (c (#) ( seq_id u))

      proof

        let c be Complex;

        let u be VECTOR of l1;

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

        set L1 = Linear_Space_of_ComplexSequences ;

        set W = the_set_of_BoundedComplexSequences ;

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

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

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

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

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

        .= (c * 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 Lm5, 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 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.|| = ( upper_bound ( rng |.( 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 :: CSSPACE4:3

    

     Th3: for x,y be Point of Complex_linfty_Space , c be Complex holds ( ||.x.|| = 0 iff x = ( 0. Complex_linfty_Space )) & 0 <= ||.x.|| & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) & ||.(c * x).|| = ( |.c.| * ||.x.||)

    proof

      let x,y be Point of Complex_linfty_Space ;

      let c be Complex;

      

       A1: for n be Nat holds ( |.(c (#) ( seq_id x)).| . n) = ( |.c.| * ( |.( seq_id x).| . n))

      proof

        let n be Nat;

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

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

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

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

        hence thesis;

      end;

      ( |.( seq_id x).| . 1) = |.(( seq_id x) . 1).| by VALUED_1: 18;

      then

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

      

       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 Th2

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

       A7:

      now

        

         A8: x in the_set_of_ComplexSequences by Def1;

        assume

         A9: ||.x.|| = 0 ;

         ||.x.|| = ( upper_bound ( rng |.( seq_id x).|)) & ( seq_id x) is bounded by Th2;

        then for n be Nat holds 0c = (( seq_id x) . n) by A9, Lm10;

        hence x = ( 0. Complex_linfty_Space ) by A8, Th2, CSSPACE: 5;

      end;

      ( seq_id x) is bounded by Def1;

      then |.( seq_id x).| is bounded by Lm8;

      then

       A10: 0 <= ( upper_bound ( rng |.( seq_id x).|)) by A2, Lm2;

      ( seq_id y) is bounded by Def1;

      then

       A11: |.( seq_id y).| is bounded by Lm8;

      ( seq_id x) is bounded by Def1;

      then |.( seq_id x).| is bounded by Lm8;

      then ( rng |.( seq_id x).|) is real-bounded by MEASURE6: 39;

      then

       A12: ( rng |.( seq_id x).|) is bounded_above;

       A13:

      now

        assume x = ( 0. Complex_linfty_Space );

        then

         A14: for n be Nat holds (( seq_id x) . n) = 0c by Th2;

        

        thus ||.x.|| = ( upper_bound ( rng |.( seq_id x).|)) by Th2

        .= 0 by A14, Lm7;

      end;

      ( seq_id x) is bounded by Def1;

      then

       A15: |.( seq_id x).| is bounded by Lm8;

      now

        let n be Nat;

        

         A16: ( |.( seq_id y).| . n) <= ( upper_bound ( rng |.( seq_id y).|)) by A11, Lm2;

        (( |.( seq_id x).| + |.( seq_id y).|) . n) = (( |.( seq_id x).| . n) + ( |.( seq_id y).| . n)) & ( |.( seq_id x).| . n) <= ( upper_bound ( rng |.( seq_id x).|)) by A15, Lm2, SEQ_1: 7;

        then

         A17: (( |.( seq_id x).| + |.( seq_id y).|) . n) <= (( upper_bound ( rng |.( seq_id x).|)) + ( upper_bound ( rng |.( seq_id y).|))) by A16, XREAL_1: 7;

        ( |.( seq_id (x + y)).| . n) <= (( |.( seq_id x).| + |.( seq_id y).|) . n) by A6;

        hence ( |.( seq_id (x + y)).| . n) <= (( upper_bound ( rng |.( seq_id x).|)) + ( upper_bound ( rng |.( seq_id y).|))) by A17, XXREAL_0: 2;

      end;

      then

       A18: ( upper_bound ( rng |.( seq_id (x + y)).|)) <= (( upper_bound ( rng |.( seq_id x).|)) + ( upper_bound ( rng |.( seq_id y).|))) by Lm1;

      

       A19: ||.y.|| = ( upper_bound ( rng |.( seq_id y).|)) & ( upper_bound ( rng |.( seq_id (x + y)).|)) = ||.(x + y).|| by Th2;

       ||.(c * x).|| = ( upper_bound ( rng |.( seq_id (c * x)).|)) by Th2

      .= ( upper_bound ( rng |.( seq_id (c (#) ( seq_id x))).|)) by Th2

      .= ( upper_bound ( rng ( |.c.| (#) |.( seq_id x).|))) by A1, SEQ_1: 9

      .= ( upper_bound ( |.c.| ** ( rng |.( seq_id x).|))) by INTEGRA2: 17

      .= ( |.c.| * ( upper_bound ( rng |.( seq_id x).|))) by A12, COMPLEX1: 46, INTEGRA2: 13

      .= ( |.c.| * ||.x.||) by Th2;

      hence thesis by A7, A13, A10, A19, A18, Th2;

    end;

    registration

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

      coherence by Th3, CLVECT_1:def 13;

    end

    

     Lm11: for seq1,seq2,seq3 be Complex_Sequence holds seq1 = (seq2 - seq3) iff for n be Nat holds (seq1 . n) = ((seq2 . n) - (seq3 . n))

    proof

      let seq1,seq2,seq3 be Complex_Sequence;

      

       A1: (for n be Nat holds (seq1 . n) = ((seq2 . n) - (seq3 . n))) implies seq1 = (seq2 - seq3)

      proof

        assume

         A2: for n be Nat holds (seq1 . n) = ((seq2 . n) - (seq3 . n));

        for x be object st x in NAT holds (seq1 . x) = ((seq2 - seq3) . x)

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider x as Element of NAT ;

          (seq1 . x) = ((seq2 . x) - (seq3 . x)) by A2

          .= ((seq2 . x) + ( - (seq3 . x)))

          .= ((seq2 . x) + (( - seq3) . x)) by VALUED_1: 8

          .= ((seq2 + ( - seq3)) . x) by VALUED_1: 1;

          hence thesis;

        end;

        hence thesis by FUNCT_2: 12;

      end;

      seq1 = (seq2 - seq3) implies for n be Nat holds (seq1 . n) = ((seq2 . n) - (seq3 . n))

      proof

        assume

         A3: seq1 = (seq2 - seq3);

        now

          let n be Nat;

          

           A4: n in NAT by ORDINAL1:def 12;

          (seq1 . n) = ((seq2 . n) + (( - seq3) . n)) by A3, VALUED_1: 1, A4

          .= ((seq2 . n) + ( - (seq3 . n))) by VALUED_1: 8;

          hence (seq1 . n) = ((seq2 . n) - (seq3 . n));

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: CSSPACE4:4

    

     Th4: for vseq be sequence of Complex_linfty_Space st vseq is Cauchy_sequence_by_Norm holds vseq is convergent

    proof

      let vseq be sequence of Complex_linfty_Space such that

       A1: vseq is Cauchy_sequence_by_Norm;

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

      

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

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

        consider cseqi be Complex_Sequence such that

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

        take ( lim cseqi);

        thus ( lim cseqi) 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 |.((cseqi . m) - (cseqi . k)).| < e

          proof

            reconsider ee = e as Real;

            consider k be Nat such that

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

            take k;

            let m be Nat such that

             A6: k <= m;

            

             A7: i in NAT by ORDINAL1:def 12;

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

            .= (( 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, A7

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

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

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

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

            then

             A8: |.((cseqi . m) - (cseqi . k)).| = ( |.( seq_id ((vseq . m) - (vseq . k))).| . i) by VALUED_1: 18;

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

            then |.( seq_id ((vseq . m) - (vseq . k))).| is bounded by Lm8;

            then

             A9: ( |.( seq_id ((vseq . m) - (vseq . k))).| . i) <= ( upper_bound ( rng |.( seq_id ((vseq . m) - (vseq . k))).|)) by Lm2;

             ||.((vseq . m) - (vseq . k)).|| = ( upper_bound ( rng |.( seq_id ((vseq . m) - (vseq . k))).|)) by Th2;

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

            hence thesis by A9, A8, XXREAL_0: 2;

          end;

        end;

        then cseqi 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 cseqi be Complex_Sequence st (for n be Nat holds (cseqi . n) = (( seq_id (vseq . n)) . i0)) & cseqi is convergent & (f . x) = ( lim cseqi) by A10;

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

      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 bounded & ( upper_bound ( rng |.(( seq_id tseq) - ( seq_id (vseq . n))).|)) <= e

      proof

        let e be Real such that

         A13: e > 0 ;

        consider k be Nat such that

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

        

         A15: for m,n be Nat st n >= k & m >= k holds |.( seq_id ((vseq . n) - (vseq . m))).| is bounded & ( upper_bound ( rng |.( seq_id ((vseq . n) - (vseq . m))).|)) < e

        proof

          let m,n be Nat;

          assume n >= k & m >= k;

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

          then

           A16: (the normF of Complex_linfty_Space . ((vseq . n) - (vseq . m))) < e;

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

          hence thesis by A16, Def2, Lm8;

        end;

        

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

        proof

          let n be Nat;

          

           A18: 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 Th2;

            hence thesis;

          end;

          now

            let i be Nat;

            consider cseqi be Complex_Sequence such that

             A19: for n be Nat holds (cseqi . n) = (( seq_id (vseq . n)) . i) and

             A20: cseqi is convergent & (tseq . i) = ( lim cseqi) by A11;

            now

              let rseq be Real_Sequence such that

               A21: for m be Nat holds (rseq . m) = ( |.( seq_id ((vseq . m) - (vseq . n))).| . i);

               A22:

              now

                let m be Nat;

                

                 A23: ( seq_id ((vseq . m) - (vseq . n))) = (( seq_id (vseq . m)) - ( seq_id (vseq . n))) by A18;

                

                thus (rseq . m) = ( |.( seq_id ((vseq . m) - (vseq . n))).| . i) by A21

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

                .= |.((( seq_id (vseq . m)) . i) - (( seq_id (vseq . n)) . i)).| by A23, Lm11

                .= |.((cseqi . m) - (( seq_id (vseq . n)) . i)).| by A19;

              end;

               |.((tseq . i) - (( seq_id (vseq . n)) . i)).| = |.((tseq - ( seq_id (vseq . n))) . i).| by Lm11

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

              hence rseq is convergent & ( lim rseq) = ( |.(( seq_id tseq) - ( seq_id (vseq . n))).| . i) by A20, A22, CSSPACE3: 1;

            end;

            hence for rseq be Real_Sequence st (for m be Nat holds (rseq . m) = ( |.( seq_id ((vseq . m) - (vseq . n))).| . i)) holds rseq is convergent & ( lim rseq) = ( |.(( seq_id tseq) - ( seq_id (vseq . n))).| . i);

          end;

          hence thesis;

        end;

        for n be Nat st n >= k holds |.(( seq_id tseq) - ( seq_id (vseq . n))).| is bounded & ( upper_bound ( rng |.(( seq_id tseq) - ( seq_id (vseq . n))).|)) <= e

        proof

          let n be Nat such that

           A24: n >= k;

          

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

          proof

            let i be Nat;

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

            consider rseq be Real_Sequence such that

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

            

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

            proof

              let m be Nat;

              

               A28: (rseq . m) = ( |.( seq_id ((vseq . m) - (vseq . n))).| . i) by A26;

              assume

               A29: m >= k;

              then |.( seq_id ((vseq . m) - (vseq . n))).| is bounded by A15, A24;

              then

               A30: ( |.( seq_id ((vseq . m) - (vseq . n))).| . i) <= ( upper_bound ( rng |.( seq_id ((vseq . m) - (vseq . n))).|)) by Lm2;

              ( upper_bound ( rng |.( seq_id ((vseq . m) - (vseq . n))).|)) <= e by A15, A24, A29;

              hence thesis by A30, A28, XXREAL_0: 2;

            end;

            rseq is convergent & ( lim rseq) = ( |.(( seq_id tseq) - ( seq_id (vseq . n))).| . i) by A17, A26;

            hence thesis by A27, RSSPACE2: 5;

          end;

          

           A31: ( 0 + e) < (1 + e) by XREAL_1: 8;

          now

            let i be Nat;

            ( |.(( seq_id tseq) - ( seq_id (vseq . n))).| . i) <= e by A25;

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

            hence |.((( seq_id tseq) - ( seq_id (vseq . n))) . i).| < (e + 1) by A31, XXREAL_0: 2;

          end;

          then (( seq_id tseq) - ( seq_id (vseq . n))) is bounded by A13, COMSEQ_2: 8;

          hence thesis by A25, Lm1, Lm8;

        end;

        hence thesis;

      end;

      

       A32: ( seq_id tseq) is bounded

      proof

        consider m be Nat such that

         A33: for n be Nat st n >= m holds |.(( seq_id tseq) - ( seq_id (vseq . n))).| is bounded & ( upper_bound ( rng |.(( seq_id tseq) - ( seq_id (vseq . n))).|)) <= jj by A12;

        

         A34: |.(( seq_id tseq) - ( seq_id (vseq . m))).| is bounded by A33;

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

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

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

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

        then

         A35: |.( seq_id (vseq . m)).| is bounded by Lm8;

        

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

        proof

          let i be Nat;

          

           A37: i in NAT by ORDINAL1:def 12;

          

           A38: (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, A37

          .= |.((( 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 A38, COMPLEX1: 59;

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

          hence thesis by SEQ_1: 7;

        end;

        d is bounded

        proof

          reconsider r = (( upper_bound ( rng (a + b))) + 1) as Real;

          (b . 1) = |.(( seq_id (vseq . m)) . 1).| by VALUED_1: 18;

          then

           A39: 0 <= (b . 1) by COMPLEX1: 46;

          

           A40: (( upper_bound ( rng (a + b))) + 0 ) < (( upper_bound ( rng (a + b))) + 1) by XREAL_1: 8;

           A41:

          now

            let i be Nat;

            (d . i) <= ((a + b) . i) & ((a + b) . i) <= ( upper_bound ( rng (a + b))) by A34, A35, A36, Lm2;

            then

             A42: (d . i) <= ( upper_bound ( rng (a + b))) by XXREAL_0: 2;

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

            hence |.(( seq_id tseq) . i).| < r by A40, A42, XXREAL_0: 2;

          end;

          (a . 1) = |.((( seq_id tseq) - ( seq_id (vseq . m))) . 1).| by VALUED_1: 18;

          then ((a + b) . 1) = ((a . 1) + (b . 1)) & 0 <= (a . 1) by COMPLEX1: 46, SEQ_1: 7;

          then 0 <= ( upper_bound ( rng (a + b))) by A34, A35, A39, Lm2;

          then ( seq_id tseq) is bounded by A41, COMSEQ_2: 8;

          hence thesis by Lm8;

        end;

        hence thesis by Lm9;

      end;

      

       A43: tseq in the_set_of_ComplexSequences by FUNCT_2: 8;

      then

      reconsider tv = tseq as Point of Complex_linfty_Space by A32, Def1;

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

      proof

        take tv;

        let e1 be Real such that

         A44: e1 > 0 ;

        set e = (e1 / 2);

        reconsider ee = e as Real;

        consider m be Nat such that

         A45: for n be Nat st n >= m holds |.(( seq_id tseq) - ( seq_id (vseq . n))).| is bounded & ( upper_bound ( rng |.(( seq_id tseq) - ( seq_id (vseq . n))).|)) <= ee by A12, A44;

        

         A46: e < e1 by A44, XREAL_1: 216;

        now

          reconsider u = tseq as VECTOR of Complex_linfty_Space by A32, A43, Def1;

          let n be Nat;

          assume n >= m;

          then

           A47: ( upper_bound ( rng |.(( seq_id tseq) - ( seq_id (vseq . n))).|)) <= e by A45;

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

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

          then ( upper_bound ( rng |.( seq_id (u - v)).|)) = ( upper_bound ( rng |.(( seq_id tseq) - ( seq_id (vseq . n))).|)) by Th2;

          then

           A48: (the normF of Complex_linfty_Space . (u - v)) <= e by A47, Def2;

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

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

          then ||.((vseq . n) - tv).|| <= e by A48;

          hence ||.((vseq . n) - tv).|| < e1 by A46, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      hence thesis by CLVECT_1:def 15;

    end;

    theorem :: CSSPACE4:5

     Complex_linfty_Space is ComplexBanachSpace by Th4, CLOPBAN1:def 13;

    begin

    definition

      let X be non empty set;

      let Y be ComplexNormSpace;

      let IT be Function of X, the carrier of Y;

      :: CSSPACE4:def4

      attr IT is bounded means

      : Def4: ex K be Real st 0 <= K & for x be Element of X holds ||.(IT . x).|| <= K;

    end

    theorem :: CSSPACE4:6

    

     Th6: for X be non empty set, Y be ComplexNormSpace, f be Function of X, the carrier of Y st (for x be Element of X holds (f . x) = ( 0. Y)) holds f is bounded

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      let f be Function of X, the carrier of Y such that

       A1: for x be Element of X holds (f . x) = ( 0. Y);

       A2:

      now

        let x be Element of X;

        

        thus ||.(f . x).|| = ||.( 0. Y).|| by A1

        .= 0 ;

      end;

      take 0 ;

      thus thesis by A2;

    end;

    registration

      let X be non empty set;

      let Y be ComplexNormSpace;

      cluster bounded for Function of X, the carrier of Y;

      existence

      proof

        set f = (X --> ( 0. Y));

        reconsider f as Function of X, the carrier of Y;

        take f;

        for x be Element of X holds (f . x) = ( 0. Y) by FUNCOP_1: 7;

        hence thesis by Th6;

      end;

    end

    definition

      let X be non empty set;

      let Y be ComplexNormSpace;

      :: CSSPACE4:def5

      func ComplexBoundedFunctions (X,Y) -> Subset of ( ComplexVectSpace (X,Y)) means

      : Def5: for x be set holds x in it iff x is bounded Function of X, the carrier of Y;

      existence

      proof

        defpred P[ object] means $1 is bounded Function of X, the carrier of Y;

        consider IT be set such that

         A1: for x be object holds x in IT iff x in ( Funcs (X,the carrier of Y)) & P[x] from XBOOLE_0:sch 1;

        take IT;

        for x be object st x in IT holds x in ( Funcs (X,the carrier of Y)) by A1;

        hence IT is Subset of ( ComplexVectSpace (X,Y)) by TARSKI:def 3;

        let x be set;

        thus x in IT implies x is bounded Function of X, the carrier of Y by A1;

        assume

         A2: x is bounded Function of X, the carrier of Y;

        then x in ( Funcs (X,the carrier of Y)) by FUNCT_2: 8;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of ( ComplexVectSpace (X,Y));

        assume that

         A3: for x be set holds x in X1 iff x is bounded Function of X, the carrier of Y and

         A4: for x be set holds x in X2 iff x is bounded Function of X, the carrier of Y;

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

        proof

          let x be object;

          assume x in X2;

          then x is bounded Function of X, the carrier of Y by A4;

          hence thesis by A3;

        end;

        then

         A5: X2 c= X1;

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

        proof

          let x be object;

          assume x in X1;

          then x is bounded Function of X, the carrier of Y by A3;

          hence thesis by A4;

        end;

        then X1 c= X2;

        hence thesis by A5;

      end;

    end

    registration

      let X be non empty set;

      let Y be ComplexNormSpace;

      cluster ( ComplexBoundedFunctions (X,Y)) -> non empty;

      coherence

      proof

        set f = (X --> ( 0. Y));

        reconsider f as Function of X, the carrier of Y;

        for x be Element of X holds (f . x) = ( 0. Y) by FUNCOP_1: 7;

        then f is bounded by Th6;

        hence thesis by Def5;

      end;

    end

    theorem :: CSSPACE4:7

    

     Th7: for X be non empty set holds for Y be ComplexNormSpace holds ( ComplexBoundedFunctions (X,Y)) is linearly-closed

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      set W = ( ComplexBoundedFunctions (X,Y));

      

       A1: for v,u be VECTOR of ( ComplexVectSpace (X,Y)) st v in W & u in W holds (v + u) in W

      proof

        let v,u be VECTOR of ( ComplexVectSpace (X,Y)) such that

         A2: v in W and

         A3: u in W;

        reconsider f = (v + u) as Function of X, the carrier of Y by FUNCT_2: 66;

        f is bounded

        proof

          reconsider v1 = v as bounded Function of X, the carrier of Y by A2, Def5;

          consider K2 be Real such that

           A4: 0 <= K2 and

           A5: for x be Element of X holds ||.(v1 . x).|| <= K2 by Def4;

          reconsider u1 = u as bounded Function of X, the carrier of Y by A3, Def5;

          consider K1 be Real such that

           A6: 0 <= K1 and

           A7: for x be Element of X holds ||.(u1 . x).|| <= K1 by Def4;

          take K3 = (K1 + K2);

          now

            let x be Element of X;

             ||.(u1 . x).|| <= K1 & ||.(v1 . x).|| <= K2 by A7, A5;

            then

             A8: ( ||.(u1 . x).|| + ||.(v1 . x).||) <= (K1 + K2) by XREAL_1: 7;

             ||.(f . x).|| = ||.((v1 . x) + (u1 . x)).|| & ||.((u1 . x) + (v1 . x)).|| <= ( ||.(u1 . x).|| + ||.(v1 . x).||) by CLOPBAN1: 11, CLVECT_1:def 13;

            hence ||.(f . x).|| <= K3 by A8, XXREAL_0: 2;

          end;

          hence thesis by A6, A4;

        end;

        hence thesis by Def5;

      end;

      for c be Complex holds for v be VECTOR of ( ComplexVectSpace (X,Y)) st v in W holds (c * v) in W

      proof

        let c be Complex;

        let v be VECTOR of ( ComplexVectSpace (X,Y)) such that

         A9: v in W;

        reconsider f = (c * v) as Function of X, the carrier of Y by FUNCT_2: 66;

        f is bounded

        proof

          reconsider v1 = v as bounded Function of X, the carrier of Y by A9, Def5;

          consider K be Real such that

           A10: 0 <= K and

           A11: for x be Element of X holds ||.(v1 . x).|| <= K by Def4;

          take ( |.c.| * K);

           A12:

          now

            let x be Element of X;

            

             A13: 0 <= |.c.| by COMPLEX1: 46;

             ||.(f . x).|| = ||.(c * (v1 . x)).|| & ||.(c * (v1 . x)).|| = ( |.c.| * ||.(v1 . x).||) by CLOPBAN1: 12, CLVECT_1:def 13;

            hence ||.(f . x).|| <= ( |.c.| * K) by A11, A13, XREAL_1: 64;

          end;

           0 <= |.c.| by COMPLEX1: 46;

          hence thesis by A10, A12;

        end;

        hence thesis by Def5;

      end;

      hence thesis by A1, CLVECT_1:def 7;

    end;

    theorem :: CSSPACE4:8

    for X be non empty set holds for Y be ComplexNormSpace holds CLSStruct (# ( ComplexBoundedFunctions (X,Y)), ( Zero_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))), ( Add_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))), ( Mult_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))) #) is Subspace of ( ComplexVectSpace (X,Y)) by Th7, CSSPACE: 11;

    registration

      let X be non empty set;

      let Y be ComplexNormSpace;

      cluster CLSStruct (# ( ComplexBoundedFunctions (X,Y)), ( Zero_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))), ( Add_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))), ( Mult_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by Th7, CSSPACE: 11;

    end

    definition

      let X be non empty set;

      let Y be ComplexNormSpace;

      :: CSSPACE4:def6

      func C_VectorSpace_of_BoundedFunctions (X,Y) -> ComplexLinearSpace equals CLSStruct (# ( ComplexBoundedFunctions (X,Y)), ( Zero_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))), ( Add_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))), ( Mult_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))) #);

      coherence ;

    end

    registration

      let X be non empty set;

      let Y be ComplexNormSpace;

      cluster ( C_VectorSpace_of_BoundedFunctions (X,Y)) -> strict;

      coherence ;

    end

    theorem :: CSSPACE4:9

    

     Th9: for X be non empty set holds for Y be ComplexNormSpace, f,g,h be VECTOR of ( C_VectorSpace_of_BoundedFunctions (X,Y)), f9,g9,h9 be bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds (h = (f + g) iff for x be Element of X holds (h9 . x) = ((f9 . x) + (g9 . x)))

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      let f,g,h be VECTOR of ( C_VectorSpace_of_BoundedFunctions (X,Y));

      

       A1: ( C_VectorSpace_of_BoundedFunctions (X,Y)) is Subspace of ( ComplexVectSpace (X,Y)) by Th7, CSSPACE: 11;

      then

      reconsider f1 = f as VECTOR of ( ComplexVectSpace (X,Y)) by CLVECT_1: 29;

      reconsider h1 = h as VECTOR of ( ComplexVectSpace (X,Y)) by A1, CLVECT_1: 29;

      reconsider g1 = g as VECTOR of ( ComplexVectSpace (X,Y)) by A1, CLVECT_1: 29;

      let f9,g9,h9 be bounded Function of X, the carrier of Y such that

       A2: f9 = f & g9 = g & h9 = h;

       A3:

      now

        assume

         A4: h = (f + g);

        let x be Element of X;

        h1 = (f1 + g1) by A1, A4, CLVECT_1: 32;

        hence (h9 . x) = ((f9 . x) + (g9 . x)) by A2, CLOPBAN1: 11;

      end;

      now

        assume for x be Element of X holds (h9 . x) = ((f9 . x) + (g9 . x));

        then h1 = (f1 + g1) by A2, CLOPBAN1: 11;

        hence h = (f + g) by A1, CLVECT_1: 32;

      end;

      hence thesis by A3;

    end;

    theorem :: CSSPACE4:10

    

     Th10: for X be non empty set holds for Y be ComplexNormSpace, f,h be VECTOR of ( C_VectorSpace_of_BoundedFunctions (X,Y)), f9,h9 be bounded Function of X, the carrier of Y st f9 = f & h9 = h holds for c be Complex holds h = (c * f) iff for x be Element of X holds (h9 . x) = (c * (f9 . x))

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      let f,h be VECTOR of ( C_VectorSpace_of_BoundedFunctions (X,Y));

      let f9,h9 be bounded Function of X, the carrier of Y such that

       A1: f9 = f & h9 = h;

      let c be Complex;

      

       A2: ( C_VectorSpace_of_BoundedFunctions (X,Y)) is Subspace of ( ComplexVectSpace (X,Y)) by Th7, CSSPACE: 11;

      then

      reconsider f1 = f, h1 = h as VECTOR of ( ComplexVectSpace (X,Y)) by CLVECT_1: 29;

       A3:

      now

        assume

         A4: h = (c * f);

        let x be Element of X;

        h1 = (c * f1) by A2, A4, CLVECT_1: 33;

        hence (h9 . x) = (c * (f9 . x)) by A1, CLOPBAN1: 12;

      end;

      now

        assume for x be Element of X holds (h9 . x) = (c * (f9 . x));

        then h1 = (c * f1) by A1, CLOPBAN1: 12;

        hence h = (c * f) by A2, CLVECT_1: 33;

      end;

      hence thesis by A3;

    end;

    theorem :: CSSPACE4:11

    

     Th11: for X be non empty set, Y be ComplexNormSpace holds ( 0. ( C_VectorSpace_of_BoundedFunctions (X,Y))) = (X --> ( 0. Y))

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      ( C_VectorSpace_of_BoundedFunctions (X,Y)) is Subspace of ( ComplexVectSpace (X,Y)) & ( 0. ( ComplexVectSpace (X,Y))) = (X --> ( 0. Y)) by Th7, CSSPACE: 11, LOPBAN_1:def 3;

      hence thesis by CLVECT_1: 30;

    end;

    definition

      let X be non empty set;

      let Y be ComplexNormSpace;

      let f be object;

      :: CSSPACE4:def7

      func modetrans (f,X,Y) -> bounded Function of X, the carrier of Y equals

      : Def7: f;

      coherence by A1, Def5;

    end

    definition

      let X be non empty set;

      let Y be ComplexNormSpace;

      let u be Function of X, the carrier of Y;

      :: CSSPACE4:def8

      func PreNorms (u) -> non empty Subset of REAL equals the set of all ||.(u . t).|| where t be Element of X;

      coherence

      proof

        set x = the Element of X;

         A1:

        now

          let x be object;

          now

            assume x in the set of all ||.(u . t).|| where t be Element of X;

            then ex t be Element of X st x = ||.(u . t).||;

            hence x in REAL ;

          end;

          hence x in the set of all ||.(u . t).|| where t be Element of X implies x in REAL ;

        end;

         ||.(u . x).|| in the set of all ||.(u . t).|| where t be Element of X;

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    theorem :: CSSPACE4:12

    

     Th12: for X be non empty set holds for Y be ComplexNormSpace, g be bounded Function of X, the carrier of Y holds ( PreNorms g) is bounded_above

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      let g be bounded Function of X, the carrier of Y;

      consider K be Real such that 0 <= K and

       A1: for x be Element of X holds ||.(g . x).|| <= K by Def4;

      take K;

      let r be ExtReal;

      assume r in ( PreNorms g);

      then ex t be Element of X st r = ||.(g . t).||;

      hence r <= K by A1;

    end;

    theorem :: CSSPACE4:13

    for X be non empty set holds for Y be ComplexNormSpace, g be Function of X, the carrier of Y holds g is bounded iff ( PreNorms g) is bounded_above

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      let g be Function of X, the carrier of Y;

      now

        reconsider K = ( upper_bound ( PreNorms g)) as Real;

        assume

         A1: ( PreNorms g) is bounded_above;

        

         A2: 0 <= K

        proof

          consider r0 be object such that

           A3: r0 in ( PreNorms g) by XBOOLE_0:def 1;

          reconsider r0 as Real by A3;

          now

            let r be Real;

            assume r in ( PreNorms g);

            then ex t be Element of X st r = ||.(g . t).||;

            hence 0 <= r by CLVECT_1: 105;

          end;

          then 0 <= r0 by A3;

          hence thesis by A1, A3, SEQ_4:def 1;

        end;

        take K;

        now

          let t be Element of X;

           ||.(g . t).|| in ( PreNorms g);

          hence ||.(g . t).|| <= K by A1, SEQ_4:def 1;

        end;

        hence g is bounded by A2;

      end;

      hence thesis by Th12;

    end;

    definition

      let X be non empty set;

      let Y be ComplexNormSpace;

      :: CSSPACE4:def9

      func ComplexBoundedFunctionsNorm (X,Y) -> Function of ( ComplexBoundedFunctions (X,Y)), REAL means

      : Def9: for x be object st x in ( ComplexBoundedFunctions (X,Y)) holds (it . x) = ( upper_bound ( PreNorms ( modetrans (x,X,Y))));

      existence

      proof

        deffunc F( object) = ( upper_bound ( PreNorms ( modetrans ($1,X,Y))));

        

         A1: for z be object st z in ( ComplexBoundedFunctions (X,Y)) holds F(z) in REAL by XREAL_0:def 1;

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

        hence thesis;

      end;

      uniqueness

      proof

        let NORM1,NORM2 be Function of ( ComplexBoundedFunctions (X,Y)), REAL such that

         A2: for x be object st x in ( ComplexBoundedFunctions (X,Y)) holds (NORM1 . x) = ( upper_bound ( PreNorms ( modetrans (x,X,Y)))) and

         A3: for x be object st x in ( ComplexBoundedFunctions (X,Y)) holds (NORM2 . x) = ( upper_bound ( PreNorms ( modetrans (x,X,Y))));

        

         A4: for z be object st z in ( ComplexBoundedFunctions (X,Y)) holds (NORM1 . z) = (NORM2 . z)

        proof

          let z be object such that

           A5: z in ( ComplexBoundedFunctions (X,Y));

          (NORM1 . z) = ( upper_bound ( PreNorms ( modetrans (z,X,Y)))) by A2, A5;

          hence thesis by A3, A5;

        end;

        ( dom NORM1) = ( ComplexBoundedFunctions (X,Y)) & ( dom NORM2) = ( ComplexBoundedFunctions (X,Y)) by FUNCT_2:def 1;

        hence thesis by A4, FUNCT_1: 2;

      end;

    end

    theorem :: CSSPACE4:14

    

     Th14: for X be non empty set, Y be ComplexNormSpace, f be bounded Function of X, the carrier of Y holds ( modetrans (f,X,Y)) = f

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      let f be bounded Function of X, the carrier of Y;

      f in ( ComplexBoundedFunctions (X,Y)) by Def5;

      hence thesis by Def7;

    end;

    theorem :: CSSPACE4:15

    

     Th15: for X be non empty set, Y be ComplexNormSpace, f be bounded Function of X, the carrier of Y holds (( ComplexBoundedFunctionsNorm (X,Y)) . f) = ( upper_bound ( PreNorms f))

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      let f be bounded Function of X, the carrier of Y;

      reconsider f9 = f as set;

      f in ( ComplexBoundedFunctions (X,Y)) by Def5;

      

      hence (( ComplexBoundedFunctionsNorm (X,Y)) . f) = ( upper_bound ( PreNorms ( modetrans (f9,X,Y)))) by Def9

      .= ( upper_bound ( PreNorms f)) by Th14;

    end;

    definition

      let X be non empty set;

      let Y be ComplexNormSpace;

      :: CSSPACE4:def10

      func C_NormSpace_of_BoundedFunctions (X,Y) -> non empty CNORMSTR equals CNORMSTR (# ( ComplexBoundedFunctions (X,Y)), ( Zero_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))), ( Add_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))), ( Mult_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))), ( ComplexBoundedFunctionsNorm (X,Y)) #);

      coherence ;

    end

    theorem :: CSSPACE4:16

    

     Th16: for X be non empty set, Y be ComplexNormSpace holds (X --> ( 0. Y)) = ( 0. ( C_NormSpace_of_BoundedFunctions (X,Y)))

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      (X --> ( 0. Y)) = ( 0. ( C_VectorSpace_of_BoundedFunctions (X,Y))) by Th11

      .= ( 0. ( C_NormSpace_of_BoundedFunctions (X,Y)));

      hence thesis;

    end;

    theorem :: CSSPACE4:17

    

     Th17: for X be non empty set, Y be ComplexNormSpace, f be Point of ( C_NormSpace_of_BoundedFunctions (X,Y)), g be bounded Function of X, the carrier of Y st g = f holds for t be Element of X holds ||.(g . t).|| <= ||.f.||

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      let f be Point of ( C_NormSpace_of_BoundedFunctions (X,Y));

      let g be bounded Function of X, the carrier of Y such that

       A1: g = f;

      

       A2: ( PreNorms g) is non empty bounded_above by Th12;

      now

        let t be Element of X;

         ||.(g . t).|| in ( PreNorms g);

        then ||.(g . t).|| <= ( upper_bound ( PreNorms g)) by A2, SEQ_4:def 1;

        then ||.(g . t).|| <= (( ComplexBoundedFunctionsNorm (X,Y)) . g) by Th15;

        hence ||.(g . t).|| <= ||.f.|| by A1;

      end;

      hence thesis;

    end;

    theorem :: CSSPACE4:18

    for X be non empty set, Y be ComplexNormSpace, f be Point of ( C_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.||

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      let f be Point of ( C_NormSpace_of_BoundedFunctions (X,Y));

      reconsider g = f as bounded Function of X, the carrier of Y by Def5;

      consider r0 be object such that

       A1: r0 in ( PreNorms g) by XBOOLE_0:def 1;

      reconsider r0 as Real by A1;

      

       A2: ( PreNorms g) is non empty bounded_above by Th12;

      

       A3: (( ComplexBoundedFunctionsNorm (X,Y)) . f) = ( upper_bound ( PreNorms g)) by Th15;

      now

        let r be Real;

        assume r in ( PreNorms g);

        then ex t be Element of X st r = ||.(g . t).||;

        hence 0 <= r by CLVECT_1: 105;

      end;

      then 0 <= r0 by A1;

      then 0 <= ( upper_bound ( PreNorms g)) by A2, A1, SEQ_4:def 1;

      hence thesis by A3;

    end;

    theorem :: CSSPACE4:19

    

     Th19: for X be non empty set, Y be ComplexNormSpace, f be Point of ( C_NormSpace_of_BoundedFunctions (X,Y)) st f = ( 0. ( C_NormSpace_of_BoundedFunctions (X,Y))) holds 0 = ||.f.||

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      let f be Point of ( C_NormSpace_of_BoundedFunctions (X,Y)) such that

       A1: f = ( 0. ( C_NormSpace_of_BoundedFunctions (X,Y)));

      thus ||.f.|| = 0

      proof

        reconsider g = f as bounded Function of X, the carrier of Y by Def5;

        set z = (X --> ( 0. Y));

        reconsider z as Function of X, the carrier of Y;

        consider r0 be object such that

         A2: r0 in ( PreNorms g) by XBOOLE_0:def 1;

        reconsider r0 as Real by A2;

        

         A3: (for s be Real st s in ( PreNorms g) holds s <= 0 ) implies ( upper_bound ( PreNorms g)) <= 0 by SEQ_4: 45;

        

         A4: ( PreNorms g) is non empty bounded_above by Th12;

        

         A5: z = g by A1, Th16;

         A6:

        now

          let r be Real;

          assume r in ( PreNorms g);

          then

          consider t be Element of X such that

           A7: r = ||.(g . t).||;

           ||.(g . t).|| = ||.( 0. Y).|| by A5, FUNCOP_1: 7

          .= 0 ;

          hence 0 <= r & r <= 0 by A7;

        end;

        then 0 <= r0 by A2;

        then ( upper_bound ( PreNorms g)) = 0 by A6, A4, A2, A3, SEQ_4:def 1;

        then (( ComplexBoundedFunctionsNorm (X,Y)) . f) = 0 by Th15;

        hence thesis;

      end;

    end;

    theorem :: CSSPACE4:20

    

     Th20: for X be non empty set, Y be ComplexNormSpace, f,g,h be Point of ( C_NormSpace_of_BoundedFunctions (X,Y)), f9,g9,h9 be bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds (h = (f + g) iff for x be Element of X holds (h9 . x) = ((f9 . x) + (g9 . x)))

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      let f,g,h be Point of ( C_NormSpace_of_BoundedFunctions (X,Y));

      reconsider f1 = f, g1 = g, h1 = h as VECTOR of ( C_VectorSpace_of_BoundedFunctions (X,Y));

      

       A1: h = (f + g) iff h1 = (f1 + g1);

      let f9,g9,h9 be bounded Function of X, the carrier of Y;

      assume f9 = f & g9 = g & h9 = h;

      hence thesis by A1, Th9;

    end;

    theorem :: CSSPACE4:21

    

     Th21: for X be non empty set, Y be ComplexNormSpace, f,h be Point of ( C_NormSpace_of_BoundedFunctions (X,Y)), f9,h9 be bounded Function of X, the carrier of Y st f9 = f & h9 = h holds for c be Complex holds h = (c * f) iff for x be Element of X holds (h9 . x) = (c * (f9 . x))

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      let f,h be Point of ( C_NormSpace_of_BoundedFunctions (X,Y));

      let f9,h9 be bounded Function of X, the carrier of Y such that

       A1: f9 = f & h9 = h;

      reconsider h1 = h as VECTOR of ( C_VectorSpace_of_BoundedFunctions (X,Y));

      reconsider f1 = f as VECTOR of ( C_VectorSpace_of_BoundedFunctions (X,Y));

      let c be Complex;

       A2:

      now

        assume h1 = (c * f1);

        

        hence h = (( Mult_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))) . [c, f1]) by CLVECT_1:def 1

        .= (c * f) by CLVECT_1:def 1;

      end;

      now

        assume h = (c * f);

        

        hence h1 = (( Mult_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))) . [c, f]) by CLVECT_1:def 1

        .= (c * f1) by CLVECT_1:def 1;

      end;

      hence thesis by A1, A2, Th10;

    end;

    theorem :: CSSPACE4:22

    

     Th22: for X be non empty set, Y be ComplexNormSpace, f,g be Point of ( C_NormSpace_of_BoundedFunctions (X,Y)), c be Complex holds ( ||.f.|| = 0 iff f = ( 0. ( C_NormSpace_of_BoundedFunctions (X,Y)))) & ||.(c * f).|| = ( |.c.| * ||.f.||) & ||.(f + g).|| <= ( ||.f.|| + ||.g.||)

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      let f,g be Point of ( C_NormSpace_of_BoundedFunctions (X,Y));

      let c be Complex;

       A1:

      now

        assume

         A2: f = ( 0. ( C_NormSpace_of_BoundedFunctions (X,Y)));

        thus ||.f.|| = 0

        proof

          reconsider g = f as bounded Function of X, the carrier of Y by Def5;

          set z = (X --> ( 0. Y));

          reconsider z as Function of X, the carrier of Y;

          consider r0 be object such that

           A3: r0 in ( PreNorms g) by XBOOLE_0:def 1;

          reconsider r0 as Real by A3;

          

           A4: (for s be Real st s in ( PreNorms g) holds s <= 0 ) implies ( upper_bound ( PreNorms g)) <= 0 by SEQ_4: 45;

          

           A5: ( PreNorms g) is non empty bounded_above by Th12;

          

           A6: z = g by A2, Th16;

           A7:

          now

            let r be Real;

            assume r in ( PreNorms g);

            then

            consider t be Element of X such that

             A8: r = ||.(g . t).||;

             ||.(g . t).|| = ||.( 0. Y).|| by A6, FUNCOP_1: 7

            .= 0 ;

            hence 0 <= r & r <= 0 by A8;

          end;

          then 0 <= r0 by A3;

          then ( upper_bound ( PreNorms g)) = 0 by A7, A5, A3, A4, SEQ_4:def 1;

          then (( ComplexBoundedFunctionsNorm (X,Y)) . f) = 0 by Th15;

          hence thesis;

        end;

      end;

      

       A9: ||.(f + g).|| <= ( ||.f.|| + ||.g.||)

      proof

        reconsider f1 = f, g1 = g, h1 = (f + g) as bounded Function of X, the carrier of Y by Def5;

        

         A10: (for s be Real st s in ( PreNorms h1) holds s <= ( ||.f.|| + ||.g.||)) implies ( upper_bound ( PreNorms h1)) <= ( ||.f.|| + ||.g.||) by SEQ_4: 45;

         A11:

        now

          let t be Element of X;

           ||.(f1 . t).|| <= ||.f.|| & ||.(g1 . t).|| <= ||.g.|| by Th17;

          then

           A12: ( ||.(f1 . t).|| + ||.(g1 . t).||) <= ( ||.f.|| + ||.g.||) by XREAL_1: 7;

           ||.(h1 . t).|| = ||.((f1 . t) + (g1 . t)).|| & ||.((f1 . t) + (g1 . t)).|| <= ( ||.(f1 . t).|| + ||.(g1 . t).||) by Th20, CLVECT_1:def 13;

          hence ||.(h1 . t).|| <= ( ||.f.|| + ||.g.||) by A12, XXREAL_0: 2;

        end;

         A13:

        now

          let r be Real;

          assume r in ( PreNorms h1);

          then ex t be Element of X st r = ||.(h1 . t).||;

          hence r <= ( ||.f.|| + ||.g.||) by A11;

        end;

        (( ComplexBoundedFunctionsNorm (X,Y)) . (f + g)) = ( upper_bound ( PreNorms h1)) by Th15;

        hence thesis by A13, A10;

      end;

      

       A14: ||.(c * f).|| = ( |.c.| * ||.f.||)

      proof

        reconsider f1 = f, h1 = (c * f) as bounded Function of X, the carrier of Y by Def5;

        

         A15: (for s be Real st s in ( PreNorms h1) holds s <= ( |.c.| * ||.f.||)) implies ( upper_bound ( PreNorms h1)) <= ( |.c.| * ||.f.||) by SEQ_4: 45;

         A16:

        now

          let t be Element of X;

          

           A17: 0 <= |.c.| by COMPLEX1: 46;

           ||.(h1 . t).|| = ||.(c * (f1 . t)).|| & ||.(c * (f1 . t)).|| = ( |.c.| * ||.(f1 . t).||) by Th21, CLVECT_1:def 13;

          hence ||.(h1 . t).|| <= ( |.c.| * ||.f.||) by A17, Th17, XREAL_1: 64;

        end;

         A18:

        now

          let r be Real;

          assume r in ( PreNorms h1);

          then ex t be Element of X st r = ||.(h1 . t).||;

          hence r <= ( |.c.| * ||.f.||) by A16;

        end;

         A19:

        now

          per cases ;

            case

             A20: c <> 0c ;

             A21:

            now

              let t be Element of X;

              

               A22: |.(c " ).| = |.( 1r / c).| by COMPLEX1:def 4, XCMPLX_1: 215

              .= (1 / |.c.|) by COMPLEX1: 48, COMPLEX1: 67

              .= (1 * ( |.c.| " )) by XCMPLX_0:def 9

              .= ( |.c.| " );

              (h1 . t) = (c * (f1 . t)) by Th21;

              

              then

               A23: ((c " ) * (h1 . t)) = (((c " ) * c) * (f1 . t)) by CLVECT_1:def 4

              .= ( 1r * (f1 . t)) by A20, COMPLEX1:def 4, XCMPLX_0:def 7

              .= (f1 . t) by CLVECT_1:def 5;

               ||.((c " ) * (h1 . t)).|| = ( |.(c " ).| * ||.(h1 . t).||) & 0 <= |.(c " ).| by CLVECT_1:def 13, COMPLEX1: 46;

              hence ||.(f1 . t).|| <= (( |.c.| " ) * ||.(c * f).||) by A23, A22, Th17, XREAL_1: 64;

            end;

             A24:

            now

              let r be Real;

              assume r in ( PreNorms f1);

              then ex t be Element of X st r = ||.(f1 . t).||;

              hence r <= (( |.c.| " ) * ||.(c * f).||) by A21;

            end;

            

             A25: (for s be Real st s in ( PreNorms f1) holds s <= (( |.c.| " ) * ||.(c * f).||)) implies ( upper_bound ( PreNorms f1)) <= (( |.c.| " ) * ||.(c * f).||) by SEQ_4: 45;

            

             A26: 0 <= |.c.| by COMPLEX1: 46;

            (( ComplexBoundedFunctionsNorm (X,Y)) . f) = ( upper_bound ( PreNorms f1)) by Th15;

            then ||.f.|| <= (( |.c.| " ) * ||.(c * f).||) by A24, A25;

            then ( |.c.| * ||.f.||) <= ( |.c.| * (( |.c.| " ) * ||.(c * f).||)) by A26, XREAL_1: 64;

            then

             A27: ( |.c.| * ||.f.||) <= (( |.c.| * ( |.c.| " )) * ||.(c * f).||);

             |.c.| <> 0 by A20, COMPLEX1: 47;

            then ( |.c.| * ||.f.||) <= (1 * ||.(c * f).||) by A27, XCMPLX_0:def 7;

            hence ( |.c.| * ||.f.||) <= ||.(c * f).||;

          end;

            case

             A28: c = 0c ;

            reconsider fz = f as VECTOR of ( C_VectorSpace_of_BoundedFunctions (X,Y));

            (c * f) = (( Mult_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))) . [c, f]) by CLVECT_1:def 1

            .= (c * fz) by CLVECT_1:def 1

            .= ( 0. ( C_VectorSpace_of_BoundedFunctions (X,Y))) by A28, CLVECT_1: 1

            .= ( 0. ( C_NormSpace_of_BoundedFunctions (X,Y)));

            hence thesis by A28, Th19, COMPLEX1: 44;

          end;

        end;

        (( ComplexBoundedFunctionsNorm (X,Y)) . (c * f)) = ( upper_bound ( PreNorms h1)) by Th15;

        then ||.(c * f).|| <= ( |.c.| * ||.f.||) by A18, A15;

        hence thesis by A19, XXREAL_0: 1;

      end;

      now

        reconsider g = f as bounded Function of X, the carrier of Y by Def5;

        set z = (X --> ( 0. Y));

        reconsider z as Function of X, the carrier of Y;

        assume

         A29: ||.f.|| = 0 ;

        now

          let t be Element of X;

           ||.(g . t).|| <= ||.f.|| by Th17;

          then ||.(g . t).|| = 0 by A29, CLVECT_1: 105;

          

          hence (g . t) = ( 0. Y) by NORMSP_0:def 5

          .= (z . t) by FUNCOP_1: 7;

        end;

        then g = z by FUNCT_2: 63;

        hence f = ( 0. ( C_NormSpace_of_BoundedFunctions (X,Y))) by Th16;

      end;

      hence thesis by A1, A14, A9;

    end;

    theorem :: CSSPACE4:23

    

     Th23: for X be non empty set, Y be ComplexNormSpace holds ( C_NormSpace_of_BoundedFunctions (X,Y)) is reflexive discerning ComplexNormSpace-like

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      thus ||.( 0. ( C_NormSpace_of_BoundedFunctions (X,Y))).|| = 0 by Th22;

      for x,y be Point of ( C_NormSpace_of_BoundedFunctions (X,Y)) holds for c be Complex holds ( ||.x.|| = 0 iff x = ( 0. ( C_NormSpace_of_BoundedFunctions (X,Y)))) & ||.(c * x).|| = ( |.c.| * ||.x.||) & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) by Th22;

      hence thesis by CLVECT_1:def 13;

    end;

    theorem :: CSSPACE4:24

    

     Th24: for X be non empty set, Y be ComplexNormSpace holds ( C_NormSpace_of_BoundedFunctions (X,Y)) is ComplexNormSpace

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

       CLSStruct (# ( ComplexBoundedFunctions (X,Y)), ( Zero_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))), ( Add_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))), ( Mult_ (( ComplexBoundedFunctions (X,Y)),( ComplexVectSpace (X,Y)))) #) is ComplexLinearSpace;

      hence thesis by Th23, CSSPACE3: 2;

    end;

    registration

      let X be non empty set;

      let Y be ComplexNormSpace;

      cluster ( C_NormSpace_of_BoundedFunctions (X,Y)) -> reflexive discerning ComplexNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable;

      coherence by Th24;

    end

    theorem :: CSSPACE4:25

    

     Th25: for X be non empty set holds for Y be ComplexNormSpace, f,g,h be Point of ( C_NormSpace_of_BoundedFunctions (X,Y)), f9,g9,h9 be bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds (h = (f - g) iff for x be Element of X holds (h9 . x) = ((f9 . x) - (g9 . x)))

    proof

      let X be non empty set;

      let Y be ComplexNormSpace;

      let f,g,h be Point of ( C_NormSpace_of_BoundedFunctions (X,Y));

      let f9,g9,h9 be bounded Function of X, the carrier of Y such that

       A1: f9 = f & g9 = g & h9 = h;

       A2:

      now

        assume

         A3: for x be Element of X holds (h9 . x) = ((f9 . x) - (g9 . x));

        now

          let x be Element of X;

          (h9 . x) = ((f9 . x) - (g9 . x)) by A3;

          then ((h9 . x) + (g9 . x)) = ((f9 . x) - ((g9 . x) - (g9 . x))) by RLVECT_1: 29;

          then ((h9 . x) + (g9 . x)) = ((f9 . x) - ( 0. Y)) by RLVECT_1: 15;

          hence ((h9 . x) + (g9 . x)) = (f9 . x) by RLVECT_1: 13;

        end;

        then f = (h + g) by A1, Th20;

        then (f - g) = (h + (g - g)) by RLVECT_1:def 3;

        then (f - g) = (h + ( 0. ( C_NormSpace_of_BoundedFunctions (X,Y)))) by RLVECT_1: 15;

        hence (f - g) = h by RLVECT_1: 4;

      end;

      now

        assume h = (f - g);

        then (h + g) = (f - (g - g)) by RLVECT_1: 29;

        then (h + g) = (f - ( 0. ( C_NormSpace_of_BoundedFunctions (X,Y)))) by RLVECT_1: 15;

        then

         A4: (h + g) = f by RLVECT_1: 13;

        now

          let x be Element of X;

          (f9 . x) = ((h9 . x) + (g9 . x)) by A1, A4, Th20;

          then ((f9 . x) - (g9 . x)) = ((h9 . x) + ((g9 . x) - (g9 . x))) by RLVECT_1:def 3;

          then ((f9 . x) - (g9 . x)) = ((h9 . x) + ( 0. Y)) by RLVECT_1: 15;

          hence ((f9 . x) - (g9 . x)) = (h9 . x) by RLVECT_1: 4;

        end;

        hence for x be Element of X holds (h9 . x) = ((f9 . x) - (g9 . x));

      end;

      hence thesis by A2;

    end;

    

     Lm12: for e be Real, seq be Real_Sequence st (seq is convergent & ex k be Nat st for i be Nat st k <= i holds (seq . i) <= e) holds ( lim seq) <= e

    proof

      let e be Real;

      let seq be Real_Sequence such that

       A1: seq is convergent and

       A2: ex k be Nat st for i be Nat st k <= i holds (seq . i) <= e;

      consider k be Nat such that

       A3: for i be Nat st k <= i holds (seq . i) <= e by A2;

      reconsider ee = e as Element of REAL by XREAL_0:def 1;

      set cseq = ( seq_const e);

      

       A4: ( lim cseq) = (cseq . 0 ) by SEQ_4: 26

      .= e by SEQ_1: 57;

       A5:

      now

        let i be Nat;

        ((seq ^\ k) . i) = (seq . (k + i)) & (seq . (k + i)) <= e by A3, NAT_1: 11, NAT_1:def 3;

        hence ((seq ^\ k) . i) <= (cseq . i) by SEQ_1: 57;

      end;

      ( lim (seq ^\ k)) = ( lim seq) by A1, SEQ_4: 20;

      hence thesis by A1, A5, A4, SEQ_2: 18;

    end;

    theorem :: CSSPACE4:26

    

     Th26: for X be non empty set, Y be ComplexNormSpace st Y is complete holds for seq be sequence of ( C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent

    proof

      let X be non empty set;

      let Y be ComplexNormSpace such that

       A1: Y is complete;

      let vseq be sequence of ( C_NormSpace_of_BoundedFunctions (X,Y)) such that

       A2: vseq is Cauchy_sequence_by_Norm;

      defpred P[ set, set] means ex xseq be sequence of Y st (for n be Nat holds (xseq . n) = (( modetrans ((vseq . n),X,Y)) . $1)) & xseq is convergent & $2 = ( lim xseq);

      

       A3: for x be Element of X holds ex y be Element of Y st P[x, y]

      proof

        let x be Element of X;

        deffunc F( Nat) = (( modetrans ((vseq . $1),X,Y)) . x);

        consider xseq be sequence of Y such that

         A4: for n be Element of NAT holds (xseq . n) = F(n) from FUNCT_2:sch 4;

        

         A5: for n be Nat holds (xseq . n) = F(n)

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A4;

        end;

        take ( lim xseq);

        

         A6: for m,k be Nat holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||

        proof

          let m,k be Nat;

          

           A7: k in NAT & m in NAT by ORDINAL1:def 12;

          (vseq . k) is bounded Function of X, the carrier of Y by Def5;

          then

           A8: ( modetrans ((vseq . k),X,Y)) = (vseq . k) by Th14;

          reconsider h1 = ((vseq . m) - (vseq . k)) as bounded Function of X, the carrier of Y by Def5;

          (vseq . m) is bounded Function of X, the carrier of Y by Def5;

          then

           A9: ( modetrans ((vseq . m),X,Y)) = (vseq . m) by Th14;

          (xseq . m) = (( modetrans ((vseq . m),X,Y)) . x) & (xseq . k) = (( modetrans ((vseq . k),X,Y)) . x) by A4, A7;

          then ((xseq . m) - (xseq . k)) = (h1 . x) by A9, A8, Th25;

          hence thesis by Th17;

        end;

        now

          let e be Real such that

           A10: e > 0 ;

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

          proof

            consider k be Nat such that

             A11: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A2, A10, CSSPACE3: 8;

            take k;

            thus for n,m be Nat st n >= k & m >= k holds ||.((xseq . n) - (xseq . m)).|| < e

            proof

              let n,m be Nat;

              assume n >= k & m >= k;

              then

               A12: ||.((vseq . n) - (vseq . m)).|| < e by A11;

               ||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| by A6;

              hence thesis by A12, XXREAL_0: 2;

            end;

          end;

        end;

        then xseq is Cauchy_sequence_by_Norm by CSSPACE3: 8;

        then xseq is convergent by A1;

        hence thesis by A5;

      end;

      consider f be Function of X, the carrier of Y such that

       A13: for x be Element of X holds P[x, (f . x)] from FUNCT_2:sch 3( A3);

      reconsider tseq = f as Function of X, the carrier of Y;

      now

        let e1 be Real such that

         A14: e1 > 0 ;

        reconsider e = e1 as Real;

        consider k be Nat such that

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

        take k;

        now

          let m be Nat;

          assume m >= k;

          then

           A16: ||.(vseq . m).|| = ( ||.vseq.|| . m) & ||.((vseq . m) - (vseq . k)).|| < e by A15, NORMSP_0:def 4;

           |.( ||.(vseq . m).|| - ||.(vseq . k).||).| <= ||.((vseq . m) - (vseq . k)).|| & ||.(vseq . k).|| = ( ||.vseq.|| . k) by CLVECT_1: 110, NORMSP_0:def 4;

          hence |.(( ||.vseq.|| . m) - ( ||.vseq.|| . k)).| < e1 by A16, XXREAL_0: 2;

        end;

        hence for m be Nat st m >= k holds |.(( ||.vseq.|| . m) - ( ||.vseq.|| . k)).| < e1;

      end;

      then

       A17: ||.vseq.|| is convergent by SEQ_4: 41;

      

       A18: tseq is bounded

      proof

        take ( lim ||.vseq.||);

         A19:

        now

          let x be Element of X;

          consider xseq be sequence of Y such that

           A20: for n be Nat holds (xseq . n) = (( modetrans ((vseq . n),X,Y)) . x) and

           A21: xseq is convergent & (tseq . x) = ( lim xseq) by A13;

          

           A22: for m be Nat holds ||.(xseq . m).|| <= ||.(vseq . m).||

          proof

            let m be Nat;

            (vseq . m) is bounded Function of X, the carrier of Y & (xseq . m) = (( modetrans ((vseq . m),X,Y)) . x) by A20, Def5;

            hence thesis by Th14, Th17;

          end;

          

           A23: for n be Nat holds ( ||.xseq.|| . n) <= ( ||.vseq.|| . n)

          proof

            let n be Nat;

            ( ||.xseq.|| . n) = ||.(xseq . n).|| & ||.(xseq . n).|| <= ||.(vseq . n).|| by A22, NORMSP_0:def 4;

            hence thesis by NORMSP_0:def 4;

          end;

           ||.xseq.|| is convergent & ||.(tseq . x).|| = ( lim ||.xseq.||) by A21, CLOPBAN1: 40;

          hence ||.(tseq . x).|| <= ( lim ||.vseq.||) by A17, A23, SEQ_2: 18;

        end;

        now

          let n be Nat;

           ||.(vseq . n).|| >= 0 by CLVECT_1: 105;

          hence ( ||.vseq.|| . n) >= 0 by NORMSP_0:def 4;

        end;

        hence thesis by A17, A19, SEQ_2: 17;

      end;

      

       A24: for e be Real st e > 0 holds ex k be Nat st for n be Nat st n >= k holds for x be Element of X holds ||.((( modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e

      proof

        let e be Real;

        assume e > 0 ;

        then

        consider k be Nat such that

         A25: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A2, CSSPACE3: 8;

        take k;

        now

          let n be Nat such that

           A26: n >= k;

          now

            let x be Element of X;

            consider xseq be sequence of Y such that

             A27: for n be Nat holds (xseq . n) = (( modetrans ((vseq . n),X,Y)) . x) and

             A28: xseq is convergent & (tseq . x) = ( lim xseq) by A13;

            

             A29: for m,k be Nat holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||

            proof

              let m,k be Nat;

              (vseq . k) is bounded Function of X, the carrier of Y by Def5;

              then

               A30: ( modetrans ((vseq . k),X,Y)) = (vseq . k) by Th14;

              reconsider h1 = ((vseq . m) - (vseq . k)) as bounded Function of X, the carrier of Y by Def5;

              (vseq . m) is bounded Function of X, the carrier of Y by Def5;

              then

               A31: ( modetrans ((vseq . m),X,Y)) = (vseq . m) by Th14;

              (xseq . m) = (( modetrans ((vseq . m),X,Y)) . x) & (xseq . k) = (( modetrans ((vseq . k),X,Y)) . x) by A27;

              then ((xseq . m) - (xseq . k)) = (h1 . x) by A31, A30, Th25;

              hence thesis by Th17;

            end;

            

             A32: for m be Nat st m >= k holds ||.((xseq . n) - (xseq . m)).|| <= e

            proof

              let m be Nat;

              assume m >= k;

              then

               A33: ||.((vseq . n) - (vseq . m)).|| < e by A25, A26;

               ||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| by A29;

              hence thesis by A33, XXREAL_0: 2;

            end;

             ||.((xseq . n) - (tseq . x)).|| <= e

            proof

              deffunc F( Nat) = ||.((xseq . $1) - (xseq . n)).||;

              consider rseq be Real_Sequence such that

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

              now

                let x be object;

                assume x in NAT ;

                then

                reconsider k = x as Nat;

                

                thus (rseq . x) = ||.((xseq . k) - (xseq . n)).|| by A34

                .= ||.((xseq - (xseq . n)) . k).|| by NORMSP_1:def 4

                .= ( ||.(xseq - (xseq . n)).|| . x) by NORMSP_0:def 4;

              end;

              then

               A35: rseq = ||.(xseq - (xseq . n)).|| by FUNCT_2: 12;

              

               A36: (xseq - (xseq . n)) is convergent & ( lim (xseq - (xseq . n))) = ((tseq . x) - (xseq . n)) by A28, CLVECT_1: 115, CLVECT_1: 121;

              then

               A37: ( lim rseq) = ||.((tseq . x) - (xseq . n)).|| by A35, CLOPBAN1: 19;

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

              proof

                let m be Nat such that

                 A38: m >= k;

                (rseq . m) = ||.((xseq . m) - (xseq . n)).|| by A34

                .= ||.((xseq . n) - (xseq . m)).|| by CLVECT_1: 108;

                hence thesis by A32, A38;

              end;

              then ( lim rseq) <= e by A36, A35, Lm12, CLOPBAN1: 19;

              hence thesis by A37, CLVECT_1: 108;

            end;

            hence ||.((( modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e by A27;

          end;

          hence for x be Element of X holds ||.((( modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e;

        end;

        hence thesis;

      end;

      reconsider tseq as bounded Function of X, the carrier of Y by A18;

      reconsider tv = tseq as Point of ( C_NormSpace_of_BoundedFunctions (X,Y)) by Def5;

      

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

      proof

        let e be Real;

        assume e > 0 ;

        then

        consider k be Nat such that

         A40: for n be Nat st n >= k holds for x be Element of X holds ||.((( modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e by A24;

        now

          set g1 = tseq;

          let n be Nat such that

           A41: n >= k;

          reconsider h1 = ((vseq . n) - tv) as bounded Function of X, the carrier of Y by Def5;

          set f1 = ( modetrans ((vseq . n),X,Y));

           A42:

          now

            let t be Element of X;

            (vseq . n) is bounded Function of X, the carrier of Y by Def5;

            then ( modetrans ((vseq . n),X,Y)) = (vseq . n) by Th14;

            then ||.(h1 . t).|| = ||.((f1 . t) - (g1 . t)).|| by Th25;

            hence ||.(h1 . t).|| <= e by A40, A41;

          end;

           A43:

          now

            let r be Real;

            assume r in ( PreNorms h1);

            then ex t be Element of X st r = ||.(h1 . t).||;

            hence r <= e by A42;

          end;

          

           A44: (for s be Real st s in ( PreNorms h1) holds s <= e) implies ( upper_bound ( PreNorms h1)) <= e by SEQ_4: 45;

          (( ComplexBoundedFunctionsNorm (X,Y)) . ((vseq . n) - tv)) = ( upper_bound ( PreNorms h1)) by Th15;

          hence ||.((vseq . n) - tv).|| <= e by A43, A44;

        end;

        hence thesis;

      end;

      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 such that

         A45: e > 0 ;

        reconsider ee = e as Real;

        consider m be Nat such that

         A46: for n be Nat st n >= m holds ||.((vseq . n) - tv).|| <= (ee / 2) by A39, A45;

        

         A47: (e / 2) < e by A45, XREAL_1: 216;

        now

          let n be Nat;

          assume n >= m;

          then ||.((vseq . n) - tv).|| <= (e / 2) by A46;

          hence ||.((vseq . n) - tv).|| < e by A47, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      hence thesis by CLVECT_1:def 15;

    end;

    theorem :: CSSPACE4:27

    

     Th27: for X be non empty set, Y be ComplexBanachSpace holds ( C_NormSpace_of_BoundedFunctions (X,Y)) is ComplexBanachSpace

    proof

      let X be non empty set;

      let Y be ComplexBanachSpace;

      for seq be sequence of ( C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent by Th26;

      hence thesis by CLOPBAN1:def 13;

    end;

    registration

      let X be non empty set;

      let Y be ComplexBanachSpace;

      cluster ( C_NormSpace_of_BoundedFunctions (X,Y)) -> complete;

      coherence by Th27;

    end

    begin

    theorem :: CSSPACE4:28

    for seq1,seq2 be Complex_Sequence st seq1 is bounded & seq2 is bounded holds (seq1 + seq2) is bounded by Lm3;

    theorem :: CSSPACE4:29

    for c be Complex, seq be Complex_Sequence st seq is bounded holds (c (#) seq) is bounded by Lm4;

    theorem :: CSSPACE4:30

    for seq be Complex_Sequence holds seq is bounded iff |.seq.| is bounded by Lm8, Lm9;

    theorem :: CSSPACE4:31

    for seq1,seq2,seq3 be Complex_Sequence holds seq1 = (seq2 - seq3) iff for n be Nat holds (seq1 . n) = ((seq2 . n) - (seq3 . n)) by Lm11;