lopban_5.miz



    begin

    theorem :: LOPBAN_5:1

    

     Th1: for seq be Real_Sequence, r be Real st seq is bounded & 0 <= r holds ( lim_inf (r (#) seq)) = (r * ( lim_inf seq))

    proof

      let seq be Real_Sequence, r be Real;

      assume that

       A1: seq is bounded and

       A2: 0 <= r;

      ( inferior_realsequence seq) in ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

      then

       A3: ex f be Function st ( inferior_realsequence seq) = f & ( dom f) = NAT & ( rng f) c= REAL by FUNCT_2:def 2;

      (( inferior_realsequence seq) . 0 ) in ( rng ( inferior_realsequence seq)) by FUNCT_2: 4;

      then

      reconsider X1 = ( rng ( inferior_realsequence seq)) as non empty Subset of REAL by A3;

      now

        let n be Element of NAT ;

        consider r1 be Real such that

         A4: 0 < r1 and

         A5: for k be Nat holds |.(seq . k).| < r1 by A1, SEQ_2: 3;

        (seq ^\ n) in ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

        then ex f be Function st (seq ^\ n) = f & ( dom f) = NAT & ( rng f) c= REAL by FUNCT_2:def 2;

        then

        reconsider Y1 = ( rng (seq ^\ n)) as non empty Subset of REAL by FUNCT_2: 4;

        now

          let k be Nat;

           |.((seq ^\ n) . k).| = |.(seq . (n + k)).| by NAT_1:def 3;

          hence |.((seq ^\ n) . k).| < r1 by A5;

        end;

        then (seq ^\ n) is bounded by A4, SEQ_2: 3;

        then

         A6: Y1 is bounded_below by RINFSUP1: 6;

        (( inferior_realsequence (r (#) seq)) . n) = ( lower_bound ((r (#) seq) ^\ n)) by RINFSUP1: 36

        .= ( lower_bound (r (#) (seq ^\ n))) by SEQM_3: 21

        .= ( lower_bound (r ** Y1)) by INTEGRA2: 17

        .= (r * ( lower_bound (seq ^\ n))) by A2, A6, INTEGRA2: 15

        .= (r * (( inferior_realsequence seq) . n)) by RINFSUP1: 36;

        hence (( inferior_realsequence (r (#) seq)) . n) = ((r (#) ( inferior_realsequence seq)) . n) by SEQ_1: 9;

      end;

      then ( inferior_realsequence (r (#) seq)) = (r (#) ( inferior_realsequence seq)) by FUNCT_2: 63;

      then

       A7: ( rng ( inferior_realsequence (r (#) seq))) = (r ** X1) by INTEGRA2: 17;

      ( inferior_realsequence seq) is bounded by A1, RINFSUP1: 56;

      then X1 is bounded_above by RINFSUP1: 5;

      hence thesis by A2, A7, INTEGRA2: 13;

    end;

    theorem :: LOPBAN_5:2

    for seq be Real_Sequence, r be Real st seq is bounded & 0 <= r holds ( lim_sup (r (#) seq)) = (r * ( lim_sup seq))

    proof

      let seq be Real_Sequence, r be Real;

      assume that

       A1: seq is bounded and

       A2: 0 <= r;

      ( superior_realsequence seq) in ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

      then

       A3: ex f be Function st ( superior_realsequence seq) = f & ( dom f) = NAT & ( rng f) c= REAL by FUNCT_2:def 2;

      (( superior_realsequence seq) . 0 ) in ( rng ( superior_realsequence seq)) by FUNCT_2: 4;

      then

      reconsider X1 = ( rng ( superior_realsequence seq)) as non empty Subset of REAL by A3;

      now

        let n be Element of NAT ;

        consider r1 be Real such that

         A4: 0 < r1 and

         A5: for k be Nat holds |.(seq . k).| < r1 by A1, SEQ_2: 3;

        (seq ^\ n) in ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

        then ex f be Function st (seq ^\ n) = f & ( dom f) = NAT & ( rng f) c= REAL by FUNCT_2:def 2;

        then

        reconsider Y1 = ( rng (seq ^\ n)) as non empty Subset of REAL by FUNCT_2: 4;

        now

          let k be Nat;

           |.((seq ^\ n) . k).| = |.(seq . (n + k)).| by NAT_1:def 3;

          hence |.((seq ^\ n) . k).| < r1 by A5;

        end;

        then (seq ^\ n) is bounded by A4, SEQ_2: 3;

        then

         A6: Y1 is bounded_above by RINFSUP1: 5;

        (( superior_realsequence (r (#) seq)) . n) = ( upper_bound ((r (#) seq) ^\ n)) by RINFSUP1: 37

        .= ( upper_bound (r (#) (seq ^\ n))) by SEQM_3: 21

        .= ( upper_bound (r ** Y1)) by INTEGRA2: 17

        .= (r * ( upper_bound (seq ^\ n))) by A2, A6, INTEGRA2: 13

        .= (r * (( superior_realsequence seq) . n)) by RINFSUP1: 37;

        hence (( superior_realsequence (r (#) seq)) . n) = ((r (#) ( superior_realsequence seq)) . n) by SEQ_1: 9;

      end;

      then ( superior_realsequence (r (#) seq)) = (r (#) ( superior_realsequence seq)) by FUNCT_2: 63;

      then

       A7: ( rng ( superior_realsequence (r (#) seq))) = (r ** X1) by INTEGRA2: 17;

      ( superior_realsequence seq) is bounded by A1, RINFSUP1: 56;

      then X1 is bounded_below by RINFSUP1: 6;

      hence thesis by A2, A7, INTEGRA2: 15;

    end;

    registration

      let X be RealBanachSpace;

      cluster ( MetricSpaceNorm X) -> complete;

      coherence

      proof

        now

          let S1 be sequence of ( MetricSpaceNorm X);

          reconsider S2 = S1 as sequence of X;

          assume

           A1: S1 is Cauchy;

          S2 is Cauchy_sequence_by_Norm

          proof

            let r be Real;

            assume r > 0 ;

            then

            consider p be Nat such that

             A2: for n,m be Nat st p <= n & p <= m holds ( dist ((S1 . n),(S1 . m))) < r by A1, TBSP_1:def 4;

            now

              let n,m be Nat;

              assume p <= n & p <= m;

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

              hence ( dist ((S2 . n),(S2 . m))) < r by NORMSP_2:def 1;

            end;

            hence thesis;

          end;

          then S2 is convergent by LOPBAN_1:def 15;

          hence S1 is convergent by NORMSP_2: 5;

        end;

        hence thesis by TBSP_1:def 5;

      end;

    end

    definition

      let X be RealNormSpace, x0 be Point of X, r be Real;

      :: LOPBAN_5:def1

      func Ball (x0,r) -> Subset of X equals { x where x be Point of X : ||.(x0 - x).|| < r };

      coherence

      proof

        defpred P[ Point of X] means ||.(x0 - $1).|| < r;

        { y where y be Point of X : P[y] } c= the carrier of X from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    ::$Notion-Name

    theorem :: LOPBAN_5:3

    

     Th3: for X be RealBanachSpace, Y be SetSequence of X st ( union ( rng Y)) = the carrier of X & (for n be Nat holds (Y . n) is closed) holds ex n0 be Nat, r be Real, x0 be Point of X st 0 < r & ( Ball (x0,r)) c= (Y . n0)

    proof

      let X be RealBanachSpace, Y be SetSequence of X;

      assume that

       A1: ( union ( rng Y)) = the carrier of X and

       A2: for n be Nat holds (Y . n) is closed;

      now

        let n be Nat;

        reconsider Yn = (Y . n) as Subset of ( TopSpaceNorm X);

        (Y . n) is closed by A2;

        then Yn is closed by NORMSP_2: 15;

        then (Yn ` ) is open by TOPS_1: 3;

        hence ((Y . n) ` ) in ( Family_open_set ( MetricSpaceNorm X)) by PRE_TOPC:def 2;

      end;

      then

      consider n0 be Nat, r be Real, xx0 be Point of ( MetricSpaceNorm X) such that

       A3: 0 < r & ( Ball (xx0,r)) c= (Y . n0) by A1, NORMSP_2: 1;

      consider x0 be Point of X such that x0 = xx0 and

       A4: ( Ball (xx0,r)) = { x where x be Point of X : ||.(x0 - x).|| < r } by NORMSP_2: 2;

      ( Ball (x0,r)) = { x where x be Point of X : ||.(x0 - x).|| < r };

      hence thesis by A3, A4;

    end;

    theorem :: LOPBAN_5:4

    

     Th4: for X,Y be RealNormSpace, f be Lipschitzian LinearOperator of X, Y holds f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of X & for x be Point of X holds f is_continuous_in x

    proof

      let X,Y be RealNormSpace, f be Lipschitzian LinearOperator of X, Y;

      consider K be Real such that

       A1: 0 <= K and

       A2: for x be VECTOR of X holds ||.(f . x).|| <= (K * ||.x.||) by LOPBAN_1:def 8;

       A3:

      now

        let x,y be Point of X;

        assume that x in the carrier of X and y in the carrier of X;

        ((f /. x) - (f /. y)) = ((f . x) + (( - 1) * (f . y))) by RLVECT_1: 16;

        then ((f /. x) - (f /. y)) = ((f . x) + (f . (( - 1) * y))) by LOPBAN_1:def 5;

        then ((f /. x) - (f /. y)) = (f . (x + (( - 1) * y))) by VECTSP_1:def 20;

        then

         A4: ((f /. x) - (f /. y)) = (f . (x + ( - y))) by RLVECT_1: 16;

         ||.((f /. x) - (f /. y)).|| <= ((K * ||.(x - y).||) + ||.(x - y).||) by A2, A4, XREAL_1: 38;

        hence ||.((f /. x) - (f /. y)).|| <= ((K + 1) * ||.(x - y).||);

      end;

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

      hence f is_Lipschitzian_on the carrier of X by A1, A3, NFCONT_1:def 9;

      hence

       A5: f is_continuous_on the carrier of X by NFCONT_1: 45;

      hereby

        let x be Point of X;

        (f | the carrier of X) = f by RELSET_1: 19;

        hence f is_continuous_in x by A5, NFCONT_1:def 7;

      end;

    end;

    theorem :: LOPBAN_5:5

    

     Th5: for X be RealBanachSpace, Y be RealNormSpace, T be Subset of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st for x be Point of X holds ex K be Real st 0 <= K & for f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.(f . x).|| <= K holds ex L be Real st 0 <= L & for f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= L

    proof

      let X be RealBanachSpace, Y be RealNormSpace, T be Subset of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A1: for x be Point of X holds ex KTx be Real st 0 <= KTx & for f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.(f . x).|| <= KTx;

      per cases ;

        suppose

         A2: T <> {} ;

        deffunc S0( Point of X, Real) = ( Ball ($1,$2));

        defpred P[ Point of X, set] means $2 = { ||.(f . $1).|| where f be Lipschitzian LinearOperator of X, Y : f in T };

        

         A3: for x be Point of X holds ex y be Element of ( bool REAL ) st P[x, y]

        proof

          let x be Point of X;

          take y = { ||.(f . x).|| where f be Lipschitzian LinearOperator of X, Y : f in T };

          now

            let z be object;

            assume z in y;

            then ex f be Lipschitzian LinearOperator of X, Y st z = ||.(f . x).|| & f in T;

            hence z in REAL ;

          end;

          hence thesis by TARSKI:def 3;

        end;

        ex Ta be Function of the carrier of X, ( bool REAL ) st for x be Element of X holds P[x, (Ta . x)] from FUNCT_2:sch 3( A3);

        then

        consider Ta be Function of X, ( bool REAL ) such that

         A4: for x be Point of X holds (Ta . x) = { ||.(f . x).|| where f be Lipschitzian LinearOperator of X, Y : f in T };

        defpred P[ Nat, set] means $2 = { x where x be Point of X : (Ta . x) is bounded_above & ( upper_bound (Ta . x)) <= $1 };

        

         A5: for n be Element of NAT holds ex y be Element of ( bool the carrier of X) st P[n, y]

        proof

          let n be Element of NAT ;

          take y = { x where x be Point of X : (Ta . x) is bounded_above & ( upper_bound (Ta . x)) <= n };

          now

            let z be object;

            assume z in y;

            then ex x be Point of X st z = x & (Ta . x) is bounded_above & ( upper_bound (Ta . x)) <= n;

            hence z in the carrier of X;

          end;

          hence thesis by TARSKI:def 3;

        end;

        ex Xn be sequence of ( bool the carrier of X) st for n be Element of NAT holds P[n, (Xn . n)] from FUNCT_2:sch 3( A5);

        then

        consider Xn be sequence of ( bool the carrier of X) such that

         A6: for n be Element of NAT holds (Xn . n) = { x where x be Point of X : (Ta . x) is bounded_above & ( upper_bound (Ta . x)) <= n };

        reconsider Xn as SetSequence of X;

        

         A7: the carrier of X c= ( union ( rng Xn))

        proof

          let x be object;

          assume x in the carrier of X;

          then

          reconsider x1 = x as Point of X;

          consider KTx1 be Real such that 0 <= KTx1 and

           A8: for f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.(f . x1).|| <= KTx1 by A1;

          

           A9: (Ta . x1) = { ||.(f . x1).|| where f be Lipschitzian LinearOperator of X, Y : f in T } by A4;

          

           A10: for p be Real st p in (Ta . x1) holds p <= KTx1

          proof

            let p be Real;

            assume p in (Ta . x1);

            then ex f be Lipschitzian LinearOperator of X, Y st p = ||.(f . x1).|| & f in T by A9;

            hence thesis by A8;

          end;

          KTx1 is UpperBound of (Ta . x1)

          proof

            let p be ExtReal;

            assume p in (Ta . x1);

            then ex f be Lipschitzian LinearOperator of X, Y st p = ||.(f . x1).|| & f in T by A9;

            hence thesis by A8;

          end;

          then

           A11: (Ta . x1) is bounded_above;

          consider n be Nat such that

           A12: KTx1 < n by SEQ_4: 3;

          

           A13: n in NAT by ORDINAL1:def 12;

          consider f be object such that

           A14: f in T by A2, XBOOLE_0:def 1;

          reconsider f as Lipschitzian LinearOperator of X, Y by A14, LOPBAN_1:def 9;

           ||.(f . x1).|| in (Ta . x) by A9, A14;

          then ( upper_bound (Ta . x1)) <= KTx1 by A10, SEQ_4: 45;

          then ( upper_bound (Ta . x1)) <= n by A12, XXREAL_0: 2;

          then x1 in { z1 where z1 be Point of X : (Ta . z1) is bounded_above & ( upper_bound (Ta . z1)) <= n } by A11;

          then x1 in (Xn . n) by A6, A13;

          then x1 in ( Union Xn) by PROB_1: 12;

          hence thesis;

        end;

        

         A15: for x be Point of X holds (Ta . x) is non empty

        proof

          let x be Point of X;

          consider f0 be object such that

           A16: f0 in T by A2, XBOOLE_0:def 1;

          reconsider f0 as Lipschitzian LinearOperator of X, Y by A16, LOPBAN_1:def 9;

          (Ta . x) = { ||.(f . x).|| where f be Lipschitzian LinearOperator of X, Y : f in T } by A4;

          then ||.(f0 . x).|| in (Ta . x) by A16;

          hence thesis;

        end;

        

         A17: for n be Nat holds (Xn . n) is closed

        proof

          let n be Nat;

          

           A18: n in NAT by ORDINAL1:def 12;

          for s1 be sequence of X st ( rng s1) c= (Xn . n) & s1 is convergent holds ( lim s1) in (Xn . n)

          proof

            let s1 be sequence of X;

            assume that

             A19: ( rng s1) c= (Xn . n) and

             A20: s1 is convergent;

            

             A21: (Ta . ( lim s1)) = { ||.(f . ( lim s1)).|| where f be Lipschitzian LinearOperator of X, Y : f in T } by A4;

            

             A22: for y be Real st y in (Ta . ( lim s1)) holds y <= n

            proof

              let y be Real;

              assume y in (Ta . ( lim s1));

              then

              consider f be Lipschitzian LinearOperator of X, Y such that

               A23: y = ||.(f . ( lim s1)).|| and

               A24: f in T by A21;

              

               A25: f is_continuous_in ( lim s1) by Th4;

              

               A26: ( dom f) = the carrier of X by FUNCT_2:def 1;

              then

               A27: ( rng s1) c= ( dom f) by A19, XBOOLE_1: 1;

              then

               A28: (f /* s1) is convergent by A20, A25, NFCONT_1:def 5;

              for k be Nat holds ( ||.(f /* s1).|| . k) <= n

              proof

                let k be Nat;

                

                 A29: k in NAT by ORDINAL1:def 12;

                ( ||.(f /* s1).|| . k) = ||.((f /* s1) . k).|| by NORMSP_0:def 4;

                then

                 A30: ( ||.(f /* s1).|| . k) = ||.(f /. (s1 . k)).|| by A19, A26, FUNCT_2: 109, A29, XBOOLE_1: 1;

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

                then (s1 . k) in ( rng s1) by FUNCT_1: 3, A29;

                then (s1 . k) in (Xn . n) by A19;

                then (s1 . k) in { x where x be Point of X : (Ta . x) is bounded_above & ( upper_bound (Ta . x)) <= n } by A6, A18;

                then

                consider x be Point of X such that

                 A31: x = (s1 . k) and

                 A32: (Ta . x) is bounded_above and

                 A33: ( upper_bound (Ta . x)) <= n;

                (Ta . x) = { ||.(g . x).|| where g be Lipschitzian LinearOperator of X, Y : g in T } by A4;

                then ||.(f . (s1 . k)).|| in (Ta . (s1 . k)) by A24, A31;

                then ||.(f . (s1 . k)).|| <= ( upper_bound (Ta . (s1 . k))) by A31, A32, SEQ_4:def 1;

                hence thesis by A30, A31, A33, XXREAL_0: 2;

              end;

              then

               A34: for i be Nat st 0 <= i holds ( ||.(f /* s1).|| . i) <= n;

              (f /. ( lim s1)) = ( lim (f /* s1)) by A20, A25, A27, NFCONT_1:def 5;

              then ( lim ||.(f /* s1).||) = ||.(f /. ( lim s1)).|| by A28, LOPBAN_1: 20;

              hence thesis by A23, A28, A34, NORMSP_1: 23, RSSPACE2: 5;

            end;

            then for y be ExtReal st y in (Ta . ( lim s1)) holds y <= n;

            then

             A35: n is UpperBound of (Ta . ( lim s1)) by XXREAL_2:def 1;

            (Ta . ( lim s1)) is non empty by A15;

            then

             A36: ( upper_bound (Ta . ( lim s1))) <= n by A22, SEQ_4: 45;

            

             A37: (Xn . n) = { x where x be Point of X : (Ta . x) is bounded_above & ( upper_bound (Ta . x)) <= n } by A6, A18;

            (Ta . ( lim s1)) is bounded_above by A35;

            hence thesis by A36, A37;

          end;

          hence thesis by NFCONT_1:def 3;

        end;

        consider f be object such that

         A38: f in T by A2, XBOOLE_0:def 1;

        reconsider f as Lipschitzian LinearOperator of X, Y by A38, LOPBAN_1:def 9;

        ( union ( rng Xn)) is Subset of X by PROB_1: 11;

        then ( union ( rng Xn)) = the carrier of X by A7, XBOOLE_0:def 10;

        then

        consider n0 be Nat, r be Real, x0 be Point of X such that

         A39: 0 < r and

         A40: S0(x0,r) c= (Xn . n0) by A17, Th3;

        

         A41: n0 in NAT by ORDINAL1:def 12;

         ||.(x0 - x0).|| = ||.( 0. X).|| by RLVECT_1: 5;

        then x0 in S0(x0,r) by A39;

        then x0 in (Xn . n0) by A40;

        then x0 in { x1 where x1 be Point of X : (Ta . x1) is bounded_above & ( upper_bound (Ta . x1)) <= n0 } by A6, A41;

        then

        consider xx1 be Point of X such that

         A42: xx1 = x0 and

         A43: (Ta . xx1) is bounded_above and ( upper_bound (Ta . xx1)) <= n0;

        (Ta . xx1) = { ||.(g . xx1).|| where g be Lipschitzian LinearOperator of X, Y : g in T } by A4;

        then ||.(f . x0).|| in (Ta . x0) by A42, A38;

        then ||.(f . x0).|| <= ( upper_bound (Ta . x0)) by A42, A43, SEQ_4:def 1;

        then

         A44: 0 <= ( upper_bound (Ta . x0));

        

         A45: for x be Point of X st x <> ( 0. X) holds (((r / (2 * ||.x.||)) * x) + x0) in S0(x0,r)

        proof

          let x be Point of X;

          reconsider x1 = (( ||.x.|| " ) * x) as Point of X;

          

           A46: ||.((r / 2) * x1).|| = ( |.(r / 2).| * ||.x1.||) by NORMSP_1:def 1;

          assume x <> ( 0. X);

          then

           A47: ||.x.|| <> 0 by NORMSP_0:def 5;

           ||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.(((r / (2 * ||.x.||)) * x) + (x0 + ( - x0))).|| by RLVECT_1:def 3;

          then ||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.(((r / (2 * ||.x.||)) * x) + ( 0. X)).|| by RLVECT_1: 5;

          then ||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.((r / (2 * ||.x.||)) * x).|| by RLVECT_1:def 4;

          then ||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.(((r / 2) / ||.x.||) * x).|| by XCMPLX_1: 78;

          then

           A48: ||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.((r / 2) * x1).|| by RLVECT_1:def 7;

          

           A49: |.( ||.x.|| " ).| = ( ||.x.|| " ) by ABSVALUE:def 1;

           ||.x1.|| = ( |.( ||.x.|| " ).| * ||.x.||) by NORMSP_1:def 1;

          then ||.x1.|| = 1 by A47, A49, XCMPLX_0:def 7;

          then ||.((r / 2) * x1).|| = (r / 2) by A39, A46, ABSVALUE:def 1;

          then

           A50: ||.(x0 - (((r / (2 * ||.x.||)) * x) + x0)).|| = (r / 2) by A48, NORMSP_1: 7;

          (r / 2) < r by A39, XREAL_1: 216;

          hence thesis by A50;

        end;

        set M = ( upper_bound (Ta . x0));

        take KT = ((2 * (M + n0)) / r);

        

         A51: for f be Lipschitzian LinearOperator of X, Y st f in T holds for x be Point of X st x in S0(x0,r) holds ||.(f . x).|| <= n0

        proof

          let f be Lipschitzian LinearOperator of X, Y;

          assume

           A52: f in T;

          

           A53: n0 in NAT by ORDINAL1:def 12;

          let x be Point of X;

          assume x in S0(x0,r);

          then x in (Xn . n0) by A40;

          then x in { x1 where x1 be Point of X : (Ta . x1) is bounded_above & ( upper_bound (Ta . x1)) <= n0 } by A6, A53;

          then

          consider x1 be Point of X such that

           A54: x1 = x and

           A55: (Ta . x1) is bounded_above and

           A56: ( upper_bound (Ta . x1)) <= n0;

          (Ta . x1) = { ||.(g . x1).|| where g be Lipschitzian LinearOperator of X, Y : g in T } by A4;

          then ||.(f . x).|| in (Ta . x) by A52, A54;

          then ||.(f . x).|| <= ( upper_bound (Ta . x)) by A54, A55, SEQ_4:def 1;

          hence thesis by A54, A56, XXREAL_0: 2;

        end;

         A57:

        now

          let f be Lipschitzian LinearOperator of X, Y;

          assume

           A58: f in T;

          

           A59: for x be Point of X st x <> ( 0. X) holds ||.(f . x).|| <= (KT * ||.x.||)

          proof

            

             A60: n0 in NAT by ORDINAL1:def 12;

             ||.(x0 - x0).|| = ||.( 0. X).|| by RLVECT_1: 5;

            then x0 in S0(x0,r) by A39;

            then x0 in (Xn . n0) by A40;

            then

             A61: x0 in { x1 where x1 be Point of X : (Ta . x1) is bounded_above & ( upper_bound (Ta . x1)) <= n0 } by A6, A60;

            set nr3 = ||.(f . x0).||;

            let x be Point of X;

            set nrp1 = (r / (2 * ||.x.||));

            set nrp2 = ((2 * ||.x.||) / r);

            set nr1 = ||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).||;

            set nr2 = ||.(f . ((r / (2 * ||.x.||)) * x)).||;

             ||.( - (f . x0)).|| = ||.(f . x0).|| by NORMSP_1: 2;

            then

             A62: (nr2 - nr3) <= ||.((f . ((r / (2 * ||.x.||)) * x)) - ( - (f . x0))).|| by NORMSP_1: 8;

            assume

             A63: x <> ( 0. X);

            then

             A64: ||.(f . (((r / (2 * ||.x.||)) * x) + x0)).|| <= n0 by A51, A45, A58;

            consider x1 be Point of X such that

             A65: x1 = x0 and

             A66: (Ta . x1) is bounded_above and ( upper_bound (Ta . x1)) <= n0 by A61;

            (Ta . x1) = { ||.(g . x1).|| where g be Lipschitzian LinearOperator of X, Y : g in T } by A4;

            then ||.(f . x0).|| in (Ta . x0) by A58, A65;

            then ||.(f . x0).|| <= ( upper_bound (Ta . x0)) by A65, A66, SEQ_4:def 1;

            then

             A67: ((nrp1 * ||.(f . x).||) - M) <= ((nrp1 * ||.(f . x).||) - nr3) by XREAL_1: 10;

             ||.x.|| <> 0 by A63, NORMSP_0:def 5;

            then

             A68: ||.x.|| > 0 ;

             ||.(f . ((r / (2 * ||.x.||)) * x)).|| = ||.((r / (2 * ||.x.||)) * (f . x)).|| by LOPBAN_1:def 5;

            then ||.(f . ((r / (2 * ||.x.||)) * x)).|| = ( |.(r / (2 * ||.x.||)).| * ||.(f . x).||) by NORMSP_1:def 1;

            then ||.(f . ((r / (2 * ||.x.||)) * x)).|| = ((r / (2 * ||.x.||)) * ||.(f . x).||) by A39, ABSVALUE:def 1;

            then ||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).|| = ||.(f . (((r / (2 * ||.x.||)) * x) + x0)).|| & (((r / (2 * ||.x.||)) * ||.(f . x).||) - nr3) <= nr1 by A62, RLVECT_1: 17, VECTSP_1:def 20;

            then (((r / (2 * ||.x.||)) * ||.(f . x).||) - nr3) <= n0 by A64, XXREAL_0: 2;

            then ((nrp1 * ||.(f . x).||) - M) <= n0 by A67, XXREAL_0: 2;

            then (((nrp1 * ||.(f . x).||) + ( - M)) + M) <= (n0 + M) by XREAL_1: 6;

            then (nrp2 * (nrp1 * ||.(f . x).||)) <= (nrp2 * (n0 + M)) by A39, XREAL_1: 64;

            then

             A69: ((nrp1 * nrp2) * ||.(f . x).||) <= (nrp2 * (n0 + M));

            (2 * ||.x.||) > 0 by A68, XREAL_1: 129;

            then (1 * ||.(f . x).||) <= (nrp2 * (n0 + M)) by A39, A69, XCMPLX_1: 112;

            hence thesis;

          end;

          

           A70: for x be Point of X holds ||.(f . x).|| <= (KT * ||.x.||)

          proof

            let x be Point of X;

            now

              assume

               A71: x = ( 0. X);

              then (f . x) = (f . ( 0 * ( 0. X))) by RLVECT_1: 10;

              then (f . x) = ( 0 * (f . ( 0. X))) by LOPBAN_1:def 5;

              then

               A72: (f . x) = ( 0. Y) by RLVECT_1: 10;

               ||.x.|| = 0 by A71;

              hence thesis by A72;

            end;

            hence thesis by A59;

          end;

          thus for k be Real st k in { ||.(f . x1).|| where x1 be Point of X : ||.x1.|| <= 1 } holds k <= KT

          proof

            let k be Real;

            assume k in { ||.(f . x1).|| where x1 be Point of X : ||.x1.|| <= 1 };

            then

            consider x be Point of X such that

             A73: k = ||.(f . x).|| & ||.x.|| <= 1;

            k <= (KT * ||.x.||) & (KT * ||.x.||) <= KT by A39, A44, A70, A73, XREAL_1: 153;

            hence thesis by XXREAL_0: 2;

          end;

        end;

        for f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= KT

        proof

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

          reconsider f1 = f as Lipschitzian LinearOperator of X, Y by LOPBAN_1:def 9;

          assume f in T;

          then

           A74: for k be Real st k in ( PreNorms f1) holds k <= KT by A57;

           ||.f.|| = ( upper_bound ( PreNorms f1)) by LOPBAN_1: 30;

          hence thesis by A74, SEQ_4: 45;

        end;

        hence thesis by A39, A44;

      end;

        suppose

         A75: T = {} ;

        take 0 ;

        thus thesis by A75;

      end;

    end;

    definition

      let X,Y be RealNormSpace, H be sequence of the carrier of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), x be Point of X;

      :: LOPBAN_5:def2

      func H # x -> sequence of Y means

      : Def2: for n be Nat holds (it . n) = ((H . n) . x);

      existence

      proof

        deffunc U( Nat) = ((H . $1) . x);

        consider f be sequence of the carrier of Y such that

         A1: for n be Element of NAT holds (f . n) = U(n) from FUNCT_2:sch 4;

        take f;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let S1,S2 be sequence of Y such that

         A2: for n be Nat holds (S1 . n) = ((H . n) . x) and

         A3: for n be Nat holds (S2 . n) = ((H . n) . x);

        now

          let n be Element of NAT ;

          (S1 . n) = ((H . n) . x) by A2;

          hence (S1 . n) = (S2 . n) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: LOPBAN_5:6

    

     Th6: for X be RealBanachSpace, Y be RealNormSpace, vseq be sequence of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), tseq be Function of X, Y st (for x be Point of X holds (vseq # x) is convergent & (tseq . x) = ( lim (vseq # x))) holds tseq is Lipschitzian LinearOperator of X, Y & (for x be Point of X holds ||.(tseq . x).|| <= (( lim_inf ||.vseq.||) * ||.x.||)) & for ttseq be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds ||.ttseq.|| <= ( lim_inf ||.vseq.||)

    proof

      let X be RealBanachSpace, Y be RealNormSpace, vseq be sequence of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), tseq be Function of X, Y;

      set T = ( rng vseq);

      set RNS = ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A1: for x be Point of X holds (vseq # x) is convergent & (tseq . x) = ( lim (vseq # x));

      

       A2: for x,y be Point of X holds (tseq . (x + y)) = ((tseq . x) + (tseq . y))

      proof

        let x,y be Point of X;

        

         A3: (vseq # y) is convergent & (tseq . y) = ( lim (vseq # y)) by A1;

        

         A4: (tseq . (x + y)) = ( lim (vseq # (x + y))) by A1;

        now

          let n be Nat;

          (vseq . n) is Lipschitzian LinearOperator of X, Y & ((vseq # (x + y)) . n) = ((vseq . n) . (x + y)) by Def2, LOPBAN_1:def 9;

          then

           A5: ((vseq # (x + y)) . n) = (((vseq . n) . x) + ((vseq . n) . y)) by VECTSP_1:def 20;

          ((vseq . n) . y) = ((vseq # y) . n) by Def2;

          hence ((vseq # (x + y)) . n) = (((vseq # x) . n) + ((vseq # y) . n)) by A5, Def2;

        end;

        then

         A6: (vseq # (x + y)) = ((vseq # x) + (vseq # y)) by NORMSP_1:def 2;

        (vseq # x) is convergent & (tseq . x) = ( lim (vseq # x)) by A1;

        hence thesis by A3, A6, A4, NORMSP_1: 25;

      end;

      

       A7: for x be Point of X holds ex K be Real st 0 <= K & for f be Point of RNS st f in T holds ||.(f . x).|| <= K

      proof

        let x be Point of X;

        (vseq # x) is convergent by A1;

        then ||.(vseq # x).|| is bounded by NORMSP_1: 23, SEQ_2: 13;

        then

        consider K be Real such that

         A8: for n be Nat holds ( ||.(vseq # x).|| . n) < K by SEQ_2:def 3;

        

         A9: for f be Point of RNS st f in T holds ||.(f . x).|| <= K

        proof

          let f be Point of RNS;

          assume f in T;

          then

          consider n be object such that

           A10: n in NAT and

           A11: f = (vseq . n) by FUNCT_2: 11;

          reconsider n as Nat by A10;

          ((vseq . n) . x) = ((vseq # x) . n) by Def2;

          then ||.(f . x).|| = ( ||.(vseq # x).|| . n) by A11, NORMSP_0:def 4;

          hence thesis by A8;

        end;

        ( ||.(vseq # x).|| . 0 ) < K by A8;

        then ||.((vseq # x) . 0 ).|| < K by NORMSP_0:def 4;

        then 0 <= K;

        hence thesis by A9;

      end;

      vseq in ( Funcs ( NAT ,the carrier of RNS)) by FUNCT_2: 8;

      then ex f0 be Function st vseq = f0 & ( dom f0) = NAT & ( rng f0) c= the carrier of RNS by FUNCT_2:def 2;

      then

      consider L be Real such that

       A12: 0 <= L and

       A13: for f be Point of RNS st f in T holds ||.f.|| <= L by A7, Th5;

      

       A14: (L + 0 ) < (1 + L) by XREAL_1: 8;

      for n be Nat holds |.( ||.vseq.|| . n).| < (1 + L)

      proof

        let n be Nat;

        

         A15: n in NAT by ORDINAL1:def 12;

         ||.(vseq . n).|| <= L by A13, FUNCT_2: 4, A15;

        then ( ||.vseq.|| . n) <= L by NORMSP_0:def 4;

        then

         A16: ( ||.vseq.|| . n) < (1 + L) by A14, XXREAL_0: 2;

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

        then 0 <= ( ||.vseq.|| . n) by NORMSP_0:def 4;

        hence thesis by A16, ABSVALUE:def 1;

      end;

      then

       A17: ||.vseq.|| is bounded by A12, SEQ_2: 3;

      

       A18: for x be Point of X holds ||.(tseq . x).|| <= (( lim_inf ||.vseq.||) * ||.x.||)

      proof

        let x be Point of X;

        

         A19: ( ||.x.|| (#) ||.vseq.||) is bounded by A17, SEQM_3: 37;

        

         A20: for n be Nat holds ||.((vseq # x) . n).|| <= ( ||.(vseq . n).|| * ||.x.||)

        proof

          let n be Nat;

          ((vseq . n) . x) = ((vseq # x) . n) & (vseq . n) is Lipschitzian LinearOperator of X, Y by Def2, LOPBAN_1:def 9;

          hence thesis by LOPBAN_1: 32;

        end;

        

         A21: for n be Nat holds ( ||.(vseq # x).|| . n) <= (( ||.x.|| (#) ||.vseq.||) . n)

        proof

          let n be Nat;

          

           A22: ||.(vseq . n).|| = ( ||.vseq.|| . n) by NORMSP_0:def 4;

          ( ||.(vseq # x).|| . n) = ||.((vseq # x) . n).|| & ||.((vseq # x) . n).|| <= ( ||.(vseq . n).|| * ||.x.||) by A20, NORMSP_0:def 4;

          hence thesis by A22, SEQ_1: 9;

        end;

        

         A23: ( lim_inf ( ||.x.|| (#) ||.vseq.||)) = (( lim_inf ||.vseq.||) * ||.x.||) by A17, Th1;

        

         A24: (vseq # x) is convergent & (tseq . x) = ( lim (vseq # x)) by A1;

        then ||.(vseq # x).|| is convergent by LOPBAN_1: 20;

        then

         A25: ( lim ||.(vseq # x).||) = ( lim_inf ||.(vseq # x).||) by RINFSUP1: 89;

         ||.(vseq # x).|| is bounded by A24, LOPBAN_1: 20, SEQ_2: 13;

        then ( lim_inf ||.(vseq # x).||) <= ( lim_inf ( ||.x.|| (#) ||.vseq.||)) by A19, A21, RINFSUP1: 91;

        hence thesis by A24, A23, A25, LOPBAN_1: 20;

      end;

      now

        let s be Real;

        assume

         A26: 0 < s;

        for k be Nat holds ( 0 - s) < ( ||.vseq.|| . ( 0 + k))

        proof

          let k be Nat;

           ||.(vseq . k).|| = ( ||.vseq.|| . k) by NORMSP_0:def 4;

          then 0 <= ( ||.vseq.|| . k);

          hence thesis by A26;

        end;

        hence ex n be Nat st for k be Nat holds ( 0 - s) < ( ||.vseq.|| . (n + k));

      end;

      then

       A27: 0 <= ( lim_inf ||.vseq.||) by A17, RINFSUP1: 82;

      

       A28: for x be Point of X, r be Real holds (tseq . (r * x)) = (r * (tseq . x))

      proof

        let x be Point of X, r be Real;

        

         A29: (tseq . x) = ( lim (vseq # x)) by A1;

         A30:

        now

          let n be Nat;

          (vseq . n) is Lipschitzian LinearOperator of X, Y & ((vseq # (r * x)) . n) = ((vseq . n) . (r * x)) by Def2, LOPBAN_1:def 9;

          then ((vseq # (r * x)) . n) = (r * ((vseq . n) . x)) by LOPBAN_1:def 5;

          hence ((vseq # (r * x)) . n) = (r * ((vseq # x) . n)) by Def2;

        end;

        (tseq . (r * x)) = ( lim (vseq # (r * x))) by A1;

        then (tseq . (r * x)) = ( lim (r * (vseq # x))) by A30, NORMSP_1:def 5;

        hence thesis by A1, A29, NORMSP_1: 28;

      end;

      then

      reconsider tseq1 = tseq as Lipschitzian LinearOperator of X, Y by A2, A18, A27, LOPBAN_1:def 5, LOPBAN_1:def 8, VECTSP_1:def 20;

      for ttseq be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds ||.ttseq.|| <= ( lim_inf ||.vseq.||)

      proof

        for k be Real st k in { ||.(tseq . x1).|| where x1 be Point of X : ||.x1.|| <= 1 } holds k <= ( lim_inf ||.vseq.||)

        proof

          let k be Real;

          assume k in { ||.(tseq . x1).|| where x1 be Point of X : ||.x1.|| <= 1 };

          then

          consider x be Point of X such that

           A31: k = ||.(tseq . x).|| & ||.x.|| <= 1;

          k <= (( lim_inf ||.vseq.||) * ||.x.||) & (( lim_inf ||.vseq.||) * ||.x.||) <= ( lim_inf ||.vseq.||) by A18, A27, A31, XREAL_1: 153;

          hence thesis by XXREAL_0: 2;

        end;

        then

         A32: ( upper_bound ( PreNorms tseq1)) <= ( lim_inf ||.vseq.||) by SEQ_4: 45;

        let ttseq be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

        assume ttseq = tseq;

        hence thesis by A32, LOPBAN_1: 30;

      end;

      hence thesis by A2, A28, A18, A27, LOPBAN_1:def 5, LOPBAN_1:def 8, VECTSP_1:def 20;

    end;

    begin

    ::$Notion-Name

    theorem :: LOPBAN_5:7

    

     Th7: for X be RealBanachSpace, X0 be Subset of ( LinearTopSpaceNorm X), Y be RealBanachSpace, vseq be sequence of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & (for x be Point of X st x in X0 holds (vseq # x) is convergent) & (for x be Point of X holds ex K be Real st 0 <= K & for n be Nat holds ||.((vseq # x) . n).|| <= K) holds for x be Point of X holds (vseq # x) is convergent

    proof

      let X be RealBanachSpace, X0 be Subset of ( LinearTopSpaceNorm X), Y be RealBanachSpace, vseq be sequence of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A1: X0 is dense;

      set T = ( rng vseq);

      assume

       A2: for x be Point of X st x in X0 holds (vseq # x) is convergent;

      vseq in ( Funcs ( NAT ,the carrier of ( R_NormSpace_of_BoundedLinearOperators (X,Y)))) by FUNCT_2: 8;

      then ex f0 be Function st vseq = f0 & ( dom f0) = NAT & ( rng f0) c= the carrier of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) by FUNCT_2:def 2;

      then

      reconsider T as Subset of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A3: for x be Point of X holds ex K be Real st 0 <= K & for n be Nat holds ||.((vseq # x) . n).|| <= K;

      for x be Point of X holds ex K be Real st 0 <= K & for f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.(f . x).|| <= K

      proof

        let x be Point of X;

        consider K be Real such that

         A4: 0 <= K and

         A5: for n be Nat holds ||.((vseq # x) . n).|| <= K by A3;

        take K;

        now

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

          assume f in T;

          then

          consider n be object such that

           A6: n in NAT and

           A7: f = (vseq . n) by FUNCT_2: 11;

          reconsider n as Nat by A6;

           ||.(f . x).|| = ||.((vseq # x) . n).|| by A7, Def2;

          hence ||.(f . x).|| <= K by A5;

        end;

        hence thesis by A4;

      end;

      then

      consider L be Real such that

       A8: 0 <= L and

       A9: for f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds ||.f.|| <= L by Th5;

      set M = (1 + L);

      

       A10: (L + 0 ) < M by XREAL_1: 8;

      

       A11: for f be Lipschitzian LinearOperator of X, Y st f in T holds for x,y be Point of X holds ||.((f . x) - (f . y)).|| <= (M * ||.(x - y).||)

      proof

        let f be Lipschitzian LinearOperator of X, Y;

        reconsider f1 = f as Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) by LOPBAN_1:def 9;

        assume f in T;

        then ||.f1.|| <= L by A9;

        then

         A12: ||.f1.|| < M by A10, XXREAL_0: 2;

        let x,y be Point of X;

         ||.((f . x) - (f . y)).|| = ||.((f . x) + (( - 1) * (f . y))).|| by RLVECT_1: 16;

        then ||.((f . x) - (f . y)).|| = ||.((f . x) + (f . (( - 1) * y))).|| by LOPBAN_1:def 5;

        then ||.((f . x) - (f . y)).|| = ||.(f . (x + (( - 1) * y))).|| by VECTSP_1:def 20;

        then

         A13: ||.((f . x) - (f . y)).|| = ||.(f . (x - y)).|| by RLVECT_1: 16;

         ||.(f . (x - y)).|| <= ( ||.f1.|| * ||.(x - y).||) & ( ||.f1.|| * ||.(x - y).||) <= (M * ||.(x - y).||) by A12, LOPBAN_1: 32, XREAL_1: 64;

        hence thesis by A13, XXREAL_0: 2;

      end;

      hereby

        let x be Point of X;

        for TK1 be Real st TK1 > 0 holds ex n0 be Nat st for n,m be Nat st n >= n0 & m >= n0 holds ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1

        proof

          let TK1 be Real such that

           A14: TK1 > 0 ;

          

           A15: 0 < (TK1 / 3) by A14, XREAL_1: 222;

          set V = { z where z be Point of X : ||.(x - z).|| < (TK1 / (3 * M)) };

          V c= the carrier of X

          proof

            let s be object;

            assume s in V;

            then ex z be Point of X st s = z & ||.(x - z).|| < (TK1 / (3 * M));

            hence thesis;

          end;

          then

          reconsider V as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

          reconsider TKK = TK1 as Real;

           0 < (3 * M) by A8, XREAL_1: 129;

          then 0 < (TK1 / (3 * M)) by A14, XREAL_1: 139;

          then ||.(x - x).|| < (TKK / (3 * M)) by NORMSP_1: 6;

          then V is open & x in V by NORMSP_2: 23;

          then X0 meets V by A1, TOPS_1: 45;

          then

          consider s be object such that

           A16: s in X0 and

           A17: s in V by XBOOLE_0: 3;

          consider y be Point of X such that

           A18: s = y and

           A19: ||.(x - y).|| < (TK1 / (3 * M)) by A17;

          for s be Real st 0 < s holds ex n1 be Nat st for m1 be Nat st n1 <= m1 holds ||.(((vseq # y) . m1) - ((vseq # y) . n1)).|| < s by A2, A16, A18, LOPBAN_3: 4;

          then (vseq # y) is Cauchy_sequence_by_Norm by LOPBAN_3: 5;

          then

          consider n0 be Nat such that

           A20: for n,m be Nat st n >= n0 & m >= n0 holds ||.(((vseq # y) . n) - ((vseq # y) . m)).|| < (TK1 / 3) by A15, RSSPACE3: 8;

          take n0;

          for n,m be Nat st n >= n0 & m >= n0 holds ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1

          proof

            let n,m be Nat;

            

             A21: m in NAT by ORDINAL1:def 12;

            

             A22: n in NAT by ORDINAL1:def 12;

            reconsider f = (vseq . n) as Lipschitzian LinearOperator of X, Y by LOPBAN_1:def 9;

            reconsider g = (vseq . m) as Lipschitzian LinearOperator of X, Y by LOPBAN_1:def 9;

             ||.(((vseq # x) . n) - ((vseq # y) . m)).|| <= ( ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).||) by NORMSP_1: 10;

            then

             A23: ( ||.(((vseq # x) . n) - ((vseq # y) . m)).|| + ||.(((vseq # y) . m) - ((vseq # x) . m)).||) <= (( ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).||) + ||.(((vseq # y) . m) - ((vseq # x) . m)).||) by XREAL_1: 6;

            assume n >= n0 & m >= n0;

            then ||.(((vseq # y) . n) - ((vseq # y) . m)).|| < (TK1 / 3) by A20;

            then ( ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).||) < ( ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) by XREAL_1: 8;

            then

             A24: (( ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).||) + ||.(((vseq # y) . m) - ((vseq # x) . m)).||) < (( ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).||) by XREAL_1: 8;

             ||.(((vseq # x) . m) - ((vseq # y) . m)).|| = ||.(((vseq . m) . x) - ((vseq # y) . m)).|| by Def2;

            then ||.(((vseq # x) . m) - ((vseq # y) . m)).|| = ||.((g . x) - (g . y)).|| by Def2;

            then

             A25: ||.(((vseq # x) . m) - ((vseq # y) . m)).|| <= (M * ||.(x - y).||) by A11, FUNCT_2: 4, A21;

            (M * ||.(x - y).||) < (M * (TK1 / (3 * M))) by A8, A19, XREAL_1: 68;

            then (M * ||.(x - y).||) < (TK1 / 3) by A8, XCMPLX_1: 92;

            then ||.(((vseq # x) . m) - ((vseq # y) . m)).|| < (TK1 / 3) by A25, XXREAL_0: 2;

            then ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < (TK1 / 3) by NORMSP_1: 7;

            then

             A26: (((TK1 / 3) + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).||) < (((TK1 / 3) + (TK1 / 3)) + (TK1 / 3)) by XREAL_1: 8;

             ||.(((vseq # x) . n) - ((vseq # y) . n)).|| = ||.(((vseq . n) . x) - ((vseq # y) . n)).|| by Def2;

            then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| = ||.((f . x) - (f . y)).|| by Def2;

            then

             A27: ||.(((vseq # x) . n) - ((vseq # y) . n)).|| <= (M * ||.(x - y).||) by A11, FUNCT_2: 4, A22;

             ||.(((vseq # x) . n) - ((vseq # x) . m)).|| <= ( ||.(((vseq # x) . n) - ((vseq # y) . m)).|| + ||.(((vseq # y) . m) - ((vseq # x) . m)).||) by NORMSP_1: 10;

            then ||.(((vseq # x) . n) - ((vseq # x) . m)).|| <= (( ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).||) + ||.(((vseq # y) . m) - ((vseq # x) . m)).||) by A23, XXREAL_0: 2;

            then

             A28: ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < (( ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).||) by A24, XXREAL_0: 2;

            (M * ||.(x - y).||) < (M * (TK1 / (3 * M))) by A8, A19, XREAL_1: 68;

            then (M * ||.(x - y).||) < (TK1 / 3) by A8, XCMPLX_1: 92;

            then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| < (TK1 / 3) by A27, XXREAL_0: 2;

            then ( ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) < ((TK1 / 3) + (TK1 / 3)) by XREAL_1: 8;

            then (( ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).||) < (((TK1 / 3) + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).||) by XREAL_1: 8;

            then (( ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).||) < (((TK1 / 3) + (TK1 / 3)) + (TK1 / 3)) by A26, XXREAL_0: 2;

            hence thesis by A28, XXREAL_0: 2;

          end;

          hence thesis;

        end;

        then (vseq # x) is Cauchy_sequence_by_Norm by RSSPACE3: 8;

        hence (vseq # x) is convergent by LOPBAN_1:def 15;

      end;

    end;

    theorem :: LOPBAN_5:8

    for X,Y be RealBanachSpace, X0 be Subset of ( LinearTopSpaceNorm X), vseq be sequence of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & (for x be Point of X st x in X0 holds (vseq # x) is convergent) & (for x be Point of X holds ex K be Real st 0 <= K & (for n be Nat holds ||.((vseq # x) . n).|| <= K)) holds ex tseq be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st (for x be Point of X holds (vseq # x) is convergent & (tseq . x) = ( lim (vseq # x)) & ||.(tseq . x).|| <= (( lim_inf ||.vseq.||) * ||.x.||)) & ||.tseq.|| <= ( lim_inf ||.vseq.||)

    proof

      let X,Y be RealBanachSpace, X0 be Subset of ( LinearTopSpaceNorm X), vseq be sequence of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A1: X0 is dense;

      deffunc F( Point of X) = ( lim (vseq # $1));

      assume

       A2: for x be Point of X st x in X0 holds (vseq # x) is convergent;

      consider tseq be Function of X, Y such that

       A3: for x be Point of X holds (tseq . x) = F(x) from FUNCT_2:sch 4;

      assume for x be Point of X holds ex K be Real st 0 <= K & for n be Nat holds ||.((vseq # x) . n).|| <= K;

      then

       A4: for x be Point of X holds (vseq # x) is convergent by A1, A2, Th7;

      then

      reconsider tseq as Lipschitzian LinearOperator of X, Y by A3, Th6;

      reconsider tseq as Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) by LOPBAN_1:def 9;

      take tseq;

      thus thesis by A4, A3, Th6;

    end;