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

      :: RSSPACE4:def1

      func the_set_of_BoundedRealSequences -> Subset of Linear_Space_of_RealSequences means

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

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

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

        hence thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of Linear_Space_of_RealSequences ;

        assume that

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

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

        thus X1 c= X2

        proof

          let x be object;

          assume x in X1;

          then x in the_set_of_RealSequences & ( 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_RealSequences & ( seq_id x) is bounded by A3;

        hence thesis by A2;

      end;

    end

    registration

      cluster the_set_of_BoundedRealSequences -> non empty;

      coherence

      proof

        ( seq_id Zeroseq ) is bounded;

        hence thesis by Def1;

      end;

      cluster the_set_of_BoundedRealSequences -> linearly-closed;

      coherence

      proof

        set W = the_set_of_BoundedRealSequences ;

        

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

        proof

          let a be Real;

          let v be VECTOR of Linear_Space_of_RealSequences ;

          assume v in W;

          then

           A2: ( seq_id v) is bounded by Def1;

          ( seq_id (a * v)) = (a (#) ( seq_id v)) by RSSPACE: 3;

          then ( seq_id (a * v)) is bounded by A2, SEQM_3: 37;

          hence thesis by Def1;

        end;

        for v,u be VECTOR of Linear_Space_of_RealSequences st v in the_set_of_BoundedRealSequences & u in the_set_of_BoundedRealSequences holds (v + u) in the_set_of_BoundedRealSequences

        proof

          let v,u be VECTOR of Linear_Space_of_RealSequences ;

          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 v) + ( seq_id u)) by RSSPACE: 2;

          hence thesis by A3, Def1;

        end;

        hence thesis by A1, RLSUB_1:def 1;

      end;

    end

    

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

    registration

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

      coherence by RSSPACE: 11;

    end

    

     Lm4: RLSStruct (# the_set_of_BoundedRealSequences , ( Zero_ ( the_set_of_BoundedRealSequences , Linear_Space_of_RealSequences )), ( Add_ ( the_set_of_BoundedRealSequences , Linear_Space_of_RealSequences )), ( Mult_ ( the_set_of_BoundedRealSequences , Linear_Space_of_RealSequences )) #) is Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

    definition

      :: RSSPACE4:def2

      func linfty_norm -> Function of the_set_of_BoundedRealSequences , REAL means

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

      existence

      proof

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

        

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

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

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

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

        

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

        proof

          let z be object such that

           A5: z in the_set_of_BoundedRealSequences ;

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

          hence thesis by A3, A5;

        end;

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

        hence thesis by A4, FUNCT_1: 2;

      end;

    end

    

     Lm5: for rseq be Real_Sequence st for n be Nat holds (rseq . n) = ( In ( 0 , REAL )) holds rseq is bounded & ( upper_bound ( rng ( abs rseq))) = 0

    proof

      let rseq be Real_Sequence such that

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

      

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

      proof

        let n be Nat;

        

         A3: (( abs rseq) . n) = |.(rseq . n).| by SEQ_1: 12;

        (rseq . n) = 0 by A1;

        hence thesis by A3, ABSVALUE: 2;

      end;

      ( rng ( abs rseq)) c= { 0 }

      proof

        let y be object;

        assume y in ( rng ( abs rseq));

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

        then y = 0 by A2;

        hence thesis by TARSKI:def 1;

      end;

      then

       A4: ( rng ( abs rseq)) = { 0 } by ZFMISC_1: 33;

      rseq is constant by A1, VALUED_0:def 18;

      hence thesis by A4, SEQ_4: 9;

    end;

    

     Lm6: for rseq be Real_Sequence st rseq is bounded & ( upper_bound ( rng ( abs rseq))) = 0 holds for n be Nat holds (rseq . n) = 0

    proof

      let rseq be Real_Sequence such that

       A1: rseq is bounded & ( upper_bound ( rng ( abs rseq))) = 0 ;

      let n be Nat;

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

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

      then (( abs rseq) . n) = 0 by A1, Lm2;

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

      hence thesis by ABSVALUE: 2;

    end;

    theorem :: RSSPACE4:1

    for rseq be Real_Sequence holds rseq is bounded & ( upper_bound ( rng ( abs rseq))) = 0 iff for n be Nat holds (rseq . n) = 0 by Lm5, Lm6;

    registration

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

      coherence by Lm4, RSSPACE3: 2;

    end

    definition

      :: RSSPACE4:def3

      func linfty_Space -> non empty NORMSTR equals NORMSTR (# the_set_of_BoundedRealSequences , ( Zero_ ( the_set_of_BoundedRealSequences , Linear_Space_of_RealSequences )), ( Add_ ( the_set_of_BoundedRealSequences , Linear_Space_of_RealSequences )), ( Mult_ ( the_set_of_BoundedRealSequences , Linear_Space_of_RealSequences )), linfty_norm #);

      coherence ;

    end

    theorem :: RSSPACE4:2

    

     Th2: the carrier of linfty_Space = the_set_of_BoundedRealSequences & (for x be set holds x is VECTOR of linfty_Space iff x is Real_Sequence & ( seq_id x) is bounded) & ( 0. linfty_Space ) = Zeroseq & (for u be VECTOR of linfty_Space holds u = ( seq_id u)) & (for u,v be VECTOR of linfty_Space holds (u + v) = (( seq_id u) + ( seq_id v))) & (for r be Real holds for u be VECTOR of linfty_Space holds (r * u) = (r (#) ( seq_id u))) & (for u be VECTOR of linfty_Space holds ( - u) = ( - ( seq_id u)) & ( seq_id ( - u)) = ( - ( seq_id u))) & (for u,v be VECTOR of linfty_Space holds (u - v) = (( seq_id u) - ( seq_id v))) & (for v be VECTOR of linfty_Space holds ( seq_id v) is bounded) & for v be VECTOR of linfty_Space holds ||.v.|| = ( upper_bound ( rng ( abs ( seq_id v))))

    proof

      set l1 = linfty_Space ;

      

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

      .= Zeroseq ;

      

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

      proof

        let x be set;

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

        hence thesis by Def1;

      end;

      

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

      proof

        let u,v be VECTOR of l1;

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

        set L1 = Linear_Space_of_RealSequences ;

        set W = the_set_of_BoundedRealSequences ;

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

        then

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

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

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

        hence thesis by RSSPACE: 2;

      end;

      

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

      proof

        let r be Real;

        let u be VECTOR of l1;

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

        set L1 = Linear_Space_of_RealSequences ;

        set W = the_set_of_BoundedRealSequences ;

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

        then

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

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

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

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

        hence thesis by RSSPACE: 3;

      end;

      

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

      proof

        let u be VECTOR of l1;

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

        hence thesis;

      end;

      

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

      proof

        let u be VECTOR of l1;

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

        .= ( - ( seq_id u)) by A5;

        hence thesis;

      end;

      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 A3

        .= (( seq_id u) - ( seq_id v)) by A8;

      end;

      hence thesis by A2, A7, A3, A5, A8, A1, Def2;

    end;

    theorem :: RSSPACE4:3

    

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

    proof

      let x,y be Point of linfty_Space ;

      let a be Real;

      

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

      proof

        let n be Nat;

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

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

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

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

        hence thesis;

      end;

      (( abs ( seq_id x)) . 1) = |.(( seq_id x) . 1).| by SEQ_1: 12;

      then

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

      

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

      proof

        let n be Nat;

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

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

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

        hence thesis;

      end;

      

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

      proof

        let n be Nat;

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

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

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

        hence thesis by SEQ_1: 12;

      end;

      

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

      proof

        let n be Nat;

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

        hence thesis by A4;

      end;

       A6:

      now

        assume

         A7: x = ( 0. linfty_Space );

        

         A8: for n be Nat holds (( seq_id x) . n) = 0 by A7, Th2;

        

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

        .= 0 by A8, Lm5;

      end;

      ( seq_id x) is bounded by Def1;

      then

       A9: 0 <= ( upper_bound ( rng ( abs ( seq_id x)))) by A2, Lm2;

      ( seq_id x) is bounded by Def1;

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

      then

       A10: ( rng ( abs ( seq_id x))) is bounded_above;

       A11:

      now

        

         A12: x in the_set_of_RealSequences by Def1;

        assume

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

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

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

        hence x = ( 0. linfty_Space ) by A12, Th2, RSSPACE: 5;

      end;

      

       A14: ( seq_id y) is bounded by Def1;

      

       A15: ( seq_id x) is bounded by Def1;

      now

        let n be Nat;

        

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

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

        then

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

        (( abs ( seq_id (x + y))) . n) <= ((( abs ( seq_id x)) + ( abs ( seq_id y))) . n) by A5;

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

      end;

      then

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

      

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

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

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

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

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

      .= ( |.a.| * ( upper_bound ( rng ( abs ( seq_id x))))) by A10, COMPLEX1: 46, INTEGRA2: 13

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

      hence thesis by A11, A6, A9, A19, A18, Th2;

    end;

    registration

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

      coherence by Th3;

    end

    theorem :: RSSPACE4:4

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

    proof

      let vseq be sequence of linfty_Space such that

       A1: vseq is Cauchy_sequence_by_Norm;

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

      

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

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Nat;

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

        consider rseqi be Real_Sequence such that

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

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

        take lr;

        now

          let e be Real such that

           A4: e > 0 ;

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

          proof

            consider k be Nat such that

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

            take k;

            let m be Nat such that

             A6: k <= m;

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

            then

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

            ( 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 SEQ_1: 7

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

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

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

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

            then

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

             ||.((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 A7, A8, XXREAL_0: 2;

          end;

        end;

        then rseqi is convergent by SEQ_4: 41;

        hence thesis by A3;

      end;

      consider f be sequence of REAL such that

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

      reconsider tseq = f as Real_Sequence;

       A10:

      now

        let i be Nat;

        reconsider x = i as set;

        i in NAT by ORDINAL1:def 12;

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

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

      end;

      

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

      proof

        let e be Real such that

         A12: e > 0 ;

        reconsider e as Real;

        consider k be Nat such that

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

        

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

        proof

          let m,n be Nat;

          assume n >= k & m >= k;

          then

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

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

          hence thesis by A15, Def2;

        end;

        

         A16: 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) = (( abs (( seq_id tseq) - ( seq_id (vseq . n)))) . i)

        proof

          let n be Nat;

          

           A17: 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 rseqi be Real_Sequence such that

             A18: for n be Nat holds (rseqi . n) = (( seq_id (vseq . n)) . i) and

             A19: rseqi is convergent & (tseq . i) = ( lim rseqi) by A10;

            now

              let rseq be Real_Sequence such that

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

               A21:

              now

                let m be Nat;

                

                 A22: ( seq_id ((vseq . m) - (vseq . n))) = (( seq_id (vseq . m)) - ( seq_id (vseq . n))) by A17;

                

                thus (rseq . m) = (( abs ( seq_id ((vseq . m) - (vseq . n)))) . i) by A20

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

                .= |.((( seq_id (vseq . m)) . i) - (( seq_id (vseq . n)) . i)).| by A22, RFUNCT_2: 1

                .= |.((rseqi . m) - (( seq_id (vseq . n)) . i)).| by A18;

              end;

               |.((tseq . i) - (( seq_id (vseq . n)) . i)).| = |.((tseq - ( seq_id (vseq . n))) . i).| by RFUNCT_2: 1

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

              hence rseq is convergent & ( lim rseq) = (( abs (( seq_id tseq) - ( seq_id (vseq . n)))) . i) by A19, A21, RSSPACE3: 1;

            end;

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

          end;

          hence thesis;

        end;

        for n be Nat st n >= k holds ( abs (( 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

           A23: n >= k;

          

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

          proof

            let i be Nat;

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

            consider rseq be Real_Sequence such that

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

            

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

            proof

              let m be Nat;

              

               A27: (rseq . m) = (( abs ( seq_id ((vseq . m) - (vseq . n)))) . i) by A25;

              assume

               A28: m >= k;

              then ( abs ( seq_id ((vseq . m) - (vseq . n)))) is bounded by A14, A23;

              then

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

              ( upper_bound ( rng ( abs ( seq_id ((vseq . m) - (vseq . n)))))) <= e by A14, A23, A28;

              hence thesis by A29, A27, XXREAL_0: 2;

            end;

            rseq is convergent & ( lim rseq) = (( abs (( seq_id tseq) - ( seq_id (vseq . n)))) . i) by A16, A25;

            hence thesis by A26, RSSPACE2: 5;

          end;

          

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

          now

            let i be Nat;

            (( abs (( seq_id tseq) - ( seq_id (vseq . n)))) . i) <= e & (( abs (( seq_id tseq) - ( seq_id (vseq . n)))) . i) = |.((( seq_id tseq) - ( seq_id (vseq . n))) . i).| by A24, SEQ_1: 12;

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

          end;

          then (( seq_id tseq) - ( seq_id (vseq . n))) is bounded by A12, SEQ_2: 3;

          hence thesis by A24, Lm1;

        end;

        hence thesis;

      end;

      

       A31: ( seq_id tseq) is bounded

      proof

        consider m be Nat such that

         A32: for n be Nat st n >= m holds ( abs (( seq_id tseq) - ( seq_id (vseq . n)))) is bounded & ( upper_bound ( rng ( abs (( seq_id tseq) - ( seq_id (vseq . n)))))) <= 1 by A11;

        

         A33: ( abs (( seq_id tseq) - ( seq_id (vseq . m)))) is bounded by A32;

        set d = ( abs ( seq_id tseq));

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

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

        

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

        

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

        proof

          let i be Nat;

          

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

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

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

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

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

          then ((d . i) - (b . i)) <= (a . i) by A36, 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 SEQ_1: 12;

          then

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

          

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

           A39:

          now

            let i be Nat;

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

            then

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

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

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

          end;

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

          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 A33, A34, A37, Lm2;

          then ( seq_id tseq) is bounded by A39, SEQ_2: 3;

          hence thesis;

        end;

        hence thesis by SEQM_3: 37;

      end;

      

       A41: tseq in the_set_of_RealSequences by FUNCT_2: 8;

      then

      reconsider tv = tseq as Point of linfty_Space by A31, Def1;

      take tv;

      let e1 be Real such that

       A42: e1 > 0 ;

      set e = (e1 / 2);

      consider m be Nat such that

       A43: for n be Nat st n >= m holds |.(( seq_id tseq) - ( seq_id (vseq . n))).| is bounded & ( upper_bound ( rng ( abs (( seq_id tseq) - ( seq_id (vseq . n)))))) <= e by A11, A42, XREAL_1: 215;

      

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

      now

        reconsider u = tseq as VECTOR of linfty_Space by A31, A41, Def1;

        let n be Nat;

        assume n >= m;

        then

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

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

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

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

        then

         A46: (the normF of linfty_Space . (u - v)) <= e by A45, Def2;

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

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

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

      end;

      hence thesis;

    end;

    begin

    definition

      let X be non empty set;

      let Y be RealNormSpace;

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

      :: RSSPACE4: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 :: RSSPACE4:5

    

     Th5: for X be non empty set holds for Y be RealNormSpace holds for 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 RealNormSpace;

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

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

      end;

    end

    definition

      let X be non empty set;

      let Y be RealNormSpace;

      :: RSSPACE4:def5

      func BoundedFunctions (X,Y) -> Subset of ( RealVectSpace (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

        

         A1: ( RealVectSpace (X,Y)) = RLSStruct (# ( Funcs (X,the carrier of Y)), ( FuncZero (X,Y)), ( FuncAdd (X,Y)), ( FuncExtMult (X,Y)) #) by LOPBAN_1:def 4;

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

        consider IT be set such that

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

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

        let x be set;

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

        assume

         A3: 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 A2, A3;

      end;

      uniqueness

      proof

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

        assume that

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

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

          hence thesis by A4;

        end;

        then

         A6: 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 A4;

          hence thesis by A5;

        end;

        then X1 c= X2;

        hence thesis by A6;

      end;

    end

    registration

      let X be non empty set;

      let Y be RealNormSpace;

      cluster ( BoundedFunctions (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 Th5;

        hence thesis by Def5;

      end;

    end

    theorem :: RSSPACE4:6

    

     Th6: for X be non empty set holds for Y be RealNormSpace holds ( BoundedFunctions (X,Y)) is linearly-closed

    proof

      let X be non empty set;

      let Y be RealNormSpace;

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

      

       A1: ( RealVectSpace (X,Y)) = RLSStruct (# ( Funcs (X,the carrier of Y)), ( FuncZero (X,Y)), ( FuncAdd (X,Y)), ( FuncExtMult (X,Y)) #) by LOPBAN_1:def 4;

      

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

      proof

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

         A3: v in W and

         A4: u in W;

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

        f is bounded

        proof

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

          consider K2 be Real such that

           A5: 0 <= K2 and

           A6: 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 A4, Def5;

          consider K1 be Real such that

           A7: 0 <= K1 and

           A8: 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 A8, A6;

            then

             A9: ( ||.(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 LOPBAN_1: 11, NORMSP_1:def 1;

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

          end;

          hence thesis by A7, A5;

        end;

        hence thesis by Def5;

      end;

      for a be Real holds for v be VECTOR of ( RealVectSpace (X,Y)) st v in W holds (a * v) in W

      proof

        let a be Real;

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

         A10: v in W;

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

        f is bounded

        proof

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

          reconsider a as Real;

          consider K be Real such that

           A11: 0 <= K and

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

          reconsider aK = ( |.a.| * K) as Real;

          take aK;

           A13:

          now

            let x be Element of X;

            

             A14: 0 <= |.a.| by COMPLEX1: 46;

             ||.(f . x).|| = ||.(a * (v1 . x)).|| & ||.(a * (v1 . x)).|| = ( |.a.| * ||.(v1 . x).||) by LOPBAN_1: 12, NORMSP_1:def 1;

            hence ||.(f . x).|| <= ( |.a.| * K) by A12, A14, XREAL_1: 64;

          end;

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

          hence thesis by A11, A13;

        end;

        hence thesis by Def5;

      end;

      hence thesis by A2, RLSUB_1:def 1;

    end;

    theorem :: RSSPACE4:7

    for X be non empty set holds for Y be RealNormSpace holds RLSStruct (# ( BoundedFunctions (X,Y)), ( Zero_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))), ( Add_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))), ( Mult_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))) #) is Subspace of ( RealVectSpace (X,Y)) by Th6, RSSPACE: 11;

    registration

      let X be non empty set;

      let Y be RealNormSpace;

      cluster RLSStruct (# ( BoundedFunctions (X,Y)), ( Zero_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))), ( Add_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))), ( Mult_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by Th6, RSSPACE: 11;

    end

    definition

      let X be non empty set;

      let Y be RealNormSpace;

      :: RSSPACE4:def6

      func R_VectorSpace_of_BoundedFunctions (X,Y) -> RealLinearSpace equals RLSStruct (# ( BoundedFunctions (X,Y)), ( Zero_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))), ( Add_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))), ( Mult_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))) #);

      coherence ;

    end

    registration

      let X be non empty set;

      let Y be RealNormSpace;

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

      coherence ;

    end

    theorem :: RSSPACE4:8

    

     Th8: for X be non empty set holds for Y be RealNormSpace holds for f,g,h be VECTOR of ( R_VectorSpace_of_BoundedFunctions (X,Y)) holds for 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 RealNormSpace;

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

      

       A1: ( R_VectorSpace_of_BoundedFunctions (X,Y)) is Subspace of ( RealVectSpace (X,Y)) by Th6, RSSPACE: 11;

      then

      reconsider f1 = f as VECTOR of ( RealVectSpace (X,Y)) by RLSUB_1: 10;

      reconsider h1 = h as VECTOR of ( RealVectSpace (X,Y)) by A1, RLSUB_1: 10;

      reconsider g1 = g as VECTOR of ( RealVectSpace (X,Y)) by A1, RLSUB_1: 10;

      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, RLSUB_1: 13;

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

      end;

      now

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

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

        hence h = (f + g) by A1, RLSUB_1: 13;

      end;

      hence thesis by A3;

    end;

    theorem :: RSSPACE4:9

    

     Th9: for X be non empty set holds for Y be RealNormSpace holds for f,h be VECTOR of ( R_VectorSpace_of_BoundedFunctions (X,Y)) holds for f9,h9 be bounded Function of X, the carrier of Y st f9 = f & h9 = h holds for a be Real holds h = (a * f) iff for x be Element of X holds (h9 . x) = (a * (f9 . x))

    proof

      let X be non empty set;

      let Y be RealNormSpace;

      let f,h be VECTOR of ( R_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 a be Real;

      reconsider a as Real;

      

       A2: ( R_VectorSpace_of_BoundedFunctions (X,Y)) is Subspace of ( RealVectSpace (X,Y)) by Th6, RSSPACE: 11;

      then

      reconsider f1 = f, h1 = h as VECTOR of ( RealVectSpace (X,Y)) by RLSUB_1: 10;

       A3:

      now

        assume

         A4: h = (a * f);

        let x be Element of X;

        h1 = (a * f1) by A2, A4, RLSUB_1: 14;

        hence (h9 . x) = (a * (f9 . x)) by A1, LOPBAN_1: 12;

      end;

      now

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

        then h1 = (a * f1) by A1, LOPBAN_1: 12;

        hence h = (a * f) by A2, RLSUB_1: 14;

      end;

      hence thesis by A3;

    end;

    theorem :: RSSPACE4:10

    

     Th10: for X be non empty set holds for Y be RealNormSpace holds ( 0. ( R_VectorSpace_of_BoundedFunctions (X,Y))) = (X --> ( 0. Y))

    proof

      let X be non empty set;

      let Y be RealNormSpace;

      ( R_VectorSpace_of_BoundedFunctions (X,Y)) is Subspace of ( RealVectSpace (X,Y)) & ( 0. ( RealVectSpace (X,Y))) = (X --> ( 0. Y)) by Th6, LOPBAN_1: 13, RSSPACE: 11;

      hence thesis by RLSUB_1: 11;

    end;

    definition

      let X be non empty set;

      let Y be RealNormSpace;

      let f be object;

      :: RSSPACE4: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 RealNormSpace;

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

      :: RSSPACE4: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 :: RSSPACE4:11

    

     Th11: for X be non empty set holds for Y be RealNormSpace holds for 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 RealNormSpace;

      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 :: RSSPACE4:12

    for X be non empty set holds for Y be RealNormSpace holds for 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 RealNormSpace;

      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;

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

    end;

    definition

      let X be non empty set;

      let Y be RealNormSpace;

      :: RSSPACE4:def9

      func BoundedFunctionsNorm (X,Y) -> Function of ( BoundedFunctions (X,Y)), REAL means

      : Def9: for x be object st x in ( BoundedFunctions (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 ( BoundedFunctions (X,Y)) holds F(z) in REAL by XREAL_0:def 1;

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

        hence thesis;

      end;

      uniqueness

      proof

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

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

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

        

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

        proof

          let z be object such that

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

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

          hence thesis by A3, A5;

        end;

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

        hence thesis by A4, FUNCT_1: 2;

      end;

    end

    theorem :: RSSPACE4:13

    

     Th13: for X be non empty set holds for Y be RealNormSpace holds for 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 RealNormSpace;

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

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

      hence thesis by Def7;

    end;

    theorem :: RSSPACE4:14

    

     Th14: for X be non empty set holds for Y be RealNormSpace holds for f be bounded Function of X, the carrier of Y holds (( BoundedFunctionsNorm (X,Y)) . f) = ( upper_bound ( PreNorms f))

    proof

      let X be non empty set;

      let Y be RealNormSpace;

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

      reconsider f9 = f as set;

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

      

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

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

    end;

    definition

      let X be non empty set;

      let Y be RealNormSpace;

      :: RSSPACE4:def10

      func R_NormSpace_of_BoundedFunctions (X,Y) -> non empty NORMSTR equals NORMSTR (# ( BoundedFunctions (X,Y)), ( Zero_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))), ( Add_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))), ( Mult_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))), ( BoundedFunctionsNorm (X,Y)) #);

      coherence ;

    end

    theorem :: RSSPACE4:15

    

     Th15: for X be non empty set holds for Y be RealNormSpace holds (X --> ( 0. Y)) = ( 0. ( R_NormSpace_of_BoundedFunctions (X,Y)))

    proof

      let X be non empty set;

      let Y be RealNormSpace;

      (X --> ( 0. Y)) = ( 0. ( R_VectorSpace_of_BoundedFunctions (X,Y))) by Th10

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

      hence thesis;

    end;

    theorem :: RSSPACE4:16

    

     Th16: for X be non empty set holds for Y be RealNormSpace holds for f be Point of ( R_NormSpace_of_BoundedFunctions (X,Y)) holds for 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 RealNormSpace;

      let f be Point of ( R_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 Th11;

      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;

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

      end;

      hence thesis;

    end;

    theorem :: RSSPACE4:17

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

    proof

      let X be non empty set;

      let Y be RealNormSpace;

      let f be Point of ( R_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 Th11;

      now

        let r be Real;

        assume r in ( PreNorms g);

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

        hence 0 <= r;

      end;

      then 0 <= r0 by A1;

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

      hence thesis by Th14;

    end;

    theorem :: RSSPACE4:18

    

     Th18: for X be non empty set holds for Y be RealNormSpace holds for f be Point of ( R_NormSpace_of_BoundedFunctions (X,Y)) st f = ( 0. ( R_NormSpace_of_BoundedFunctions (X,Y))) holds 0 = ||.f.||

    proof

      let X be non empty set;

      let Y be RealNormSpace;

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

       A1: f = ( 0. ( R_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 Th11;

        

         A5: z = g by A1, Th15;

         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;

        hence thesis by Th14;

      end;

    end;

    theorem :: RSSPACE4:19

    

     Th19: for X be non empty set holds for Y be RealNormSpace holds for f,g,h be Point of ( R_NormSpace_of_BoundedFunctions (X,Y)) holds for 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 RealNormSpace;

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

      reconsider f1 = f, g1 = g, h1 = h as VECTOR of ( R_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, Th8;

    end;

    theorem :: RSSPACE4:20

    

     Th20: for X be non empty set holds for Y be RealNormSpace holds for f,h be Point of ( R_NormSpace_of_BoundedFunctions (X,Y)) holds for f9,h9 be bounded Function of X, the carrier of Y st f9 = f & h9 = h holds for a be Real holds h = (a * f) iff for x be Element of X holds (h9 . x) = (a * (f9 . x))

    proof

      let X be non empty set;

      let Y be RealNormSpace;

      let f,h be Point of ( R_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 ( R_VectorSpace_of_BoundedFunctions (X,Y));

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

      let a be Real;

      h = (a * f) iff h1 = (a * f1);

      hence thesis by A1, Th9;

    end;

    theorem :: RSSPACE4:21

    

     Th21: for X be non empty set holds for Y be RealNormSpace holds for f,g be Point of ( R_NormSpace_of_BoundedFunctions (X,Y)) holds for a be Real holds ( ||.f.|| = 0 iff f = ( 0. ( R_NormSpace_of_BoundedFunctions (X,Y)))) & ||.(a * f).|| = ( |.a.| * ||.f.||) & ||.(f + g).|| <= ( ||.f.|| + ||.g.||)

    proof

      let X be non empty set;

      let Y be RealNormSpace;

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

      let a be Real;

       A1:

      now

        assume

         A2: f = ( 0. ( R_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 Th11;

          

           A6: z = g by A2, Th15;

           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;

          hence thesis by Th14;

        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:

        now

          let t be Element of X;

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

          then

           A11: ( ||.(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 Th19, NORMSP_1:def 1;

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

        end;

         A12:

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

        end;

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

        hence thesis by A12, Th14;

      end;

      

       A13: ||.(a * f).|| = ( |.a.| * ||.f.||)

      proof

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

        

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

         A15:

        now

          let t be Element of X;

          

           A16: 0 <= |.a.| by COMPLEX1: 46;

           ||.(h1 . t).|| = ||.(a * (f1 . t)).|| & ||.(a * (f1 . t)).|| = ( |.a.| * ||.(f1 . t).||) by Th20, NORMSP_1:def 1;

          hence ||.(h1 . t).|| <= ( |.a.| * ||.f.||) by A16, Th16, XREAL_1: 64;

        end;

         A17:

        now

          let r be Real;

          assume r in ( PreNorms h1);

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

          hence r <= ( |.a.| * ||.f.||) by A15;

        end;

         A18:

        now

          per cases ;

            case

             A19: a <> 0 ;

             A20:

            now

              let t be Element of X;

              

               A21: |.(a " ).| = |.(1 * (a " )).|

              .= |.(1 / a).| by XCMPLX_0:def 9

              .= (1 / |.a.|) by ABSVALUE: 7

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

              .= ( |.a.| " );

              (h1 . t) = (a * (f1 . t)) by Th20;

              

              then

               A22: ((a " ) * (h1 . t)) = (((a " ) * a) * (f1 . t)) by RLVECT_1:def 7

              .= (1 * (f1 . t)) by A19, XCMPLX_0:def 7

              .= (f1 . t) by RLVECT_1:def 8;

               ||.((a " ) * (h1 . t)).|| = ( |.(a " ).| * ||.(h1 . t).||) & 0 <= |.(a " ).| by COMPLEX1: 46, NORMSP_1:def 1;

              hence ||.(f1 . t).|| <= (( |.a.| " ) * ||.(a * f).||) by A22, A21, Th16, XREAL_1: 64;

            end;

             A23:

            now

              let r be Real;

              assume r in ( PreNorms f1);

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

              hence r <= (( |.a.| " ) * ||.(a * f).||) by A20;

            end;

            

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

            (( BoundedFunctionsNorm (X,Y)) . f) = ( upper_bound ( PreNorms f1)) & 0 <= |.a.| by Th14, COMPLEX1: 46;

            then ( |.a.| * ||.f.||) <= ( |.a.| * (( |.a.| " ) * ||.(a * f).||)) by A23, A24, XREAL_1: 64;

            then

             A25: ( |.a.| * ||.f.||) <= (( |.a.| * ( |.a.| " )) * ||.(a * f).||);

             |.a.| <> 0 by A19, COMPLEX1: 47;

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

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

          end;

            case

             A26: a = 0 ;

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

            

             A27: (a * f) = (a * fz)

            .= ( 0. ( R_VectorSpace_of_BoundedFunctions (X,Y))) by A26, RLVECT_1: 10

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

            

            thus ( |.a.| * ||.f.||) = ( 0 * ||.f.||) by A26, ABSVALUE: 2

            .= ||.(a * f).|| by A27, Th18;

          end;

        end;

        (( BoundedFunctionsNorm (X,Y)) . (a * f)) = ( upper_bound ( PreNorms h1)) by Th14;

        hence thesis by A17, A14, A18, 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

         A28: ||.f.|| = 0 ;

        now

          let t be Element of X;

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

          then ||.(g . t).|| = 0 by A28;

          

          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. ( R_NormSpace_of_BoundedFunctions (X,Y))) by Th15;

      end;

      hence thesis by A1, A13, A9;

    end;

    theorem :: RSSPACE4:22

    

     Th22: for X be non empty set holds for Y be RealNormSpace holds ( R_NormSpace_of_BoundedFunctions (X,Y)) is reflexive discerning RealNormSpace-like by Th21;

    theorem :: RSSPACE4:23

    

     Th23: for X be non empty set holds for Y be RealNormSpace holds ( R_NormSpace_of_BoundedFunctions (X,Y)) is RealNormSpace

    proof

      let X be non empty set;

      let Y be RealNormSpace;

       RLSStruct (# ( BoundedFunctions (X,Y)), ( Zero_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))), ( Add_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))), ( Mult_ (( BoundedFunctions (X,Y)),( RealVectSpace (X,Y)))) #) is RealLinearSpace;

      hence thesis by Th22, RSSPACE3: 2;

    end;

    registration

      let X be non empty set;

      let Y be RealNormSpace;

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

      coherence by Th23;

    end

    theorem :: RSSPACE4:24

    

     Th24: for X be non empty set holds for Y be RealNormSpace holds for f,g,h be Point of ( R_NormSpace_of_BoundedFunctions (X,Y)) holds for 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 RealNormSpace;

      let f,g,h be Point of ( R_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);

        end;

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

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

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

        hence (f - g) = h;

      end;

      now

        assume h = (f - g);

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

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

        then

         A4: (h + g) = f;

        now

          let x be Element of X;

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

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

        end;

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

      end;

      hence thesis by A2;

    end;

    

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

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

        ((seq ^\ k) . ii) = (seq . (k + ii)) & (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 :: RSSPACE4:25

    

     Th25: for X be non empty set holds for Y be RealNormSpace st Y is complete holds for seq be sequence of ( R_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 RealNormSpace such that

       A1: Y is complete;

      let vseq be sequence of ( R_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;

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

          then

           A7: ( modetrans ((vseq . k),X,Y)) = (vseq . k) by Th13;

          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

           A8: ( modetrans ((vseq . m),X,Y)) = (vseq . m) by Th13;

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

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

          then ((xseq . m) - (xseq . k)) = (h1 . x) by A8, A7, Th24;

          hence thesis by Th16;

        end;

        now

          let e be Real such that

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

             A10: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A2, A9, RSSPACE3: 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

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

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

              hence thesis by A11, XXREAL_0: 2;

            end;

          end;

        end;

        then xseq is Cauchy_sequence_by_Norm by RSSPACE3: 8;

        then xseq is convergent by A1, LOPBAN_1:def 15;

        hence thesis by A5;

      end;

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

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

         A13: e1 > 0 ;

        reconsider e = e1 as Real;

        consider k be Nat such that

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

        take k;

        now

          let m be Nat;

          assume m >= k;

          then

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

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

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

        end;

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

      end;

      then

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

      

       A17: tseq is bounded

      proof

        reconsider lv = ( lim ||.vseq.||) as Real;

        take lv;

         A18:

        now

          let x be Element of X;

          consider xseq be sequence of Y such that

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

           A20: xseq is convergent & (tseq . x) = ( lim xseq) by A12;

          

           A21: 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 A19, Def5;

            hence thesis by Th13, Th16;

          end;

          

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

          proof

            let n be Nat;

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

            hence thesis by NORMSP_0:def 4;

          end;

           ||.xseq.|| is convergent & ||.(tseq . x).|| = ( lim ||.xseq.||) by A20, LOPBAN_1: 41;

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

        end;

        now

          let n be Nat;

           ||.(vseq . n).|| >= 0 ;

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

        end;

        hence thesis by A16, A18, SEQ_2: 17;

      end;

      

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

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

        take k;

        now

          let n be Nat such that

           A25: n >= k;

          now

            let x be Element of X;

            consider xseq be sequence of Y such that

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

             A27: xseq is convergent & (tseq . x) = ( lim xseq) by A12;

            

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

               A29: ( modetrans ((vseq . k),X,Y)) = (vseq . k) by Th13;

              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

               A30: ( modetrans ((vseq . m),X,Y)) = (vseq . m) by Th13;

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

              then ((xseq . m) - (xseq . k)) = (h1 . x) by A30, A29, Th24;

              hence thesis by Th16;

            end;

            

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

            proof

              let m be Nat;

              assume m >= k;

              then

               A32: ||.((vseq . n) - (vseq . m)).|| < e by A24, A25;

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

              hence thesis by A32, XXREAL_0: 2;

            end;

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

            proof

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

              consider rseq be Real_Sequence such that

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

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

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

              end;

              then

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

              

               A35: (xseq - (xseq . n)) is convergent & ( lim (xseq - (xseq . n))) = ((tseq . x) - (xseq . n)) by A27, NORMSP_1: 21, NORMSP_1: 27;

              then

               A36: ( lim rseq) = ||.((tseq . x) - (xseq . n)).|| by A34, LOPBAN_1: 20;

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

              proof

                let m be Nat such that

                 A37: m >= k;

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

                .= ||.((xseq . n) - (xseq . m)).|| by NORMSP_1: 7;

                hence thesis by A31, A37;

              end;

              then ( lim rseq) <= e by A35, A34, Lm7, LOPBAN_1: 20;

              hence thesis by A36, NORMSP_1: 7;

            end;

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

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

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

      

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

         A39: 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 A23;

        now

          set g1 = tseq;

          let n be Nat such that

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

           A41:

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

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

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

          end;

           A42:

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

          end;

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

          hence ||.((vseq . n) - tv).|| <= e by A42, Th14;

        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

         A43: e > 0 ;

        reconsider ee = e as Real;

        consider m be Nat such that

         A44: for n be Nat st n >= m holds ||.((vseq . n) - tv).|| <= (ee / 2) by A38, A43, XREAL_1: 215;

        

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

        now

          let n be Nat;

          assume n >= m;

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

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

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: RSSPACE4:26

    

     Th26: for X be non empty set holds for Y be RealBanachSpace holds ( R_NormSpace_of_BoundedFunctions (X,Y)) is RealBanachSpace

    proof

      let X be non empty set;

      let Y be RealBanachSpace;

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

      hence thesis by LOPBAN_1:def 15;

    end;

    registration

      let X be non empty set;

      let Y be RealBanachSpace;

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

      coherence by Th26;

    end