:: Uniform Boundedness Principle
::  by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama
::
:: Received October 9, 2007
:: Copyright (c) 2007 Association of Mizar Users

environ

 vocabularies TARSKI, RLVECT_1, FUNCT_1, PRE_TOPC, ARYTM, BOOLE, ABSVALUE,
      ARYTM_1, FCONT_1, FINSEQ_4, ARYTM_3, RELAT_1, SEQ_2, LATTICES, ORDINAL2,
      NORMSP_1, SUBSET_1, TOPS_1, METRIC_1, PCOMPS_1, NORMSP_2, PROB_1, BHSP_3,
      SEQ_1, SEQ_4, RINFSUP1, FUNCT_2, SEQM_3, RSSPACE3, LOPBAN_1, TDGROUP,
      MSUALG_3;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, PARTFUN1,
      PRE_TOPC, TOPS_1, STRUCT_0, ORDINAL1, CARD_3, NUMBERS, XREAL_0, RINFSUP1,
      COMPLEX1, REAL_1, NAT_1, XXREAL_0, VALUED_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4,
      PSCOMP_1, RLVECT_1, TBSP_1, METRIC_1, PCOMPS_1, NORMSP_1, NORMSP_2,
      RSSPACE3, LOPBAN_1, NFCONT_1, INTEGRA2, KURATO_2;
 constructors REAL_1, COMPLEX1, SEQ_1, SETFAM_1, TOPS_1, TBSP_1, NFCONT_1,
      FRECHET2, NAT_1, PSCOMP_1, PARTFUN1, RINFSUP1, INTEGRA2, PROB_1,
      NORMSP_2, RSSPACE3, LOPBAN_1, XXREAL_2;
 registrations NUMBERS, XREAL_0, XBOOLE_0, XXREAL_0, ORDINAL1, RELSET_1,
      STRUCT_0, MEMBERED, SUBSET_1, NAT_1, NORMSP_1, NORMSP_2, FUNCT_2,
      LOPBAN_1, VALUED_0, VALUED_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, RLVECT_1, METRIC_1, PCOMPS_1, NORMSP_2, RSSPACE3,
      LOPBAN_1, RINFSUP1, CARD_3, XCMPLX_0, NORMSP_1;
 theorems TARSKI, XBOOLE_1, SEQ_1, SEQ_2, RLVECT_1, FUNCT_2, XBOOLE_0, XREAL_1,
      XCMPLX_1, NORMSP_1, TBSP_1, PRE_TOPC, TOPS_1, NFCONT_1, XXREAL_0,
      FUNCT_1, NORMSP_2, RINFSUP1, ABSVALUE, XCMPLX_0, SEQM_3, INTEGRA2, SEQ_4,
      RSSPACE2, LOPBAN_1, LOPBAN_3, PROB_1, RSSPACE3;
 schemes FUNCT_2, FRAENKEL;

begin :: Uniform Boundedness Principle

theorem 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
A1: seq is bounded & 0<=r;
  inferior_realsequence seq in Funcs(NAT,REAL) by FUNCT_2:11;
  then
A2: 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:6;
  then reconsider X1 = rng inferior_realsequence seq as non empty Subset of
  REAL by A2;
  inferior_realsequence seq is bounded by A1,RINFSUP1:58;
  then inferior_realsequence seq is bounded_above by SEQ_2:def 5;
  then
A3: X1 is bounded_above by RINFSUP1:5;
  now
    let n be Element of NAT;
    seq ^\n in Funcs(NAT,REAL) by FUNCT_2:11;
    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:6;
    consider r1 be real number such that
A4: 0<r1 & for k be Element of NAT holds abs(seq.k)<r1 by A1,SEQ_2:15;
    now
      let k be Element of NAT;
      abs((seq ^\n).k) = abs(seq.(n+k)) by SEQM_3:def 9;
      hence abs((seq ^\n).k) < r1 by A4;
    end;
    then seq ^\n is bounded by A4,SEQ_2:15;
    then seq ^\n is bounded_below by SEQ_2:def 5;
    then
A5: Y1 is bounded_below by RINFSUP1:6;
    (inferior_realsequence (r(#)seq)).n = inf((r(#)seq)^\n) by RINFSUP1:38
      .= inf(r(#)(seq^\n)) by SEQM_3:44
      .= inf(r**Y1) by INTEGRA2:17
      .= r * inf(seq ^\n) by A1,A5,INTEGRA2:15
      .= r * (inferior_realsequence seq).n by RINFSUP1:38;
    hence (inferior_realsequence (r (#) seq)).n
    = (r (#) (inferior_realsequence seq)).n by SEQ_1:13;
  end;
  then inferior_realsequence (r (#) seq)
  = r (#) (inferior_realsequence seq) by FUNCT_2:113;
  then rng inferior_realsequence (r (#) seq) = r ** X1 by INTEGRA2:17;
  hence thesis by A1,A3,INTEGRA2:13;
end;

theorem
  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
A1: seq is bounded & 0<=r;
  superior_realsequence seq in Funcs(NAT,REAL) by FUNCT_2:11;
  then
A2: 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:6;
  then reconsider X1 = rng superior_realsequence seq
  as non empty Subset of REAL by A2;
  superior_realsequence seq is bounded by A1,RINFSUP1:58;
  then superior_realsequence seq is bounded_below by SEQ_2:def 5;
  then
A3: X1 is bounded_below by RINFSUP1:6;
  now
    let n be Element of NAT;
    seq ^\n in Funcs(NAT,REAL) by FUNCT_2:11;
    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:6;
    consider r1 be real number such that
A4: 0<r1 & for k be Element of NAT holds abs(seq.k)<r1 by A1,SEQ_2:15;
    now
      let k be Element of NAT;
      abs((seq ^\n).k) = abs(seq.(n+k)) by SEQM_3:def 9;
      hence abs((seq ^\n).k) < r1 by A4;
    end;
    then seq ^\n is bounded by A4,SEQ_2:15;
    then seq ^\n is bounded_above by SEQ_2:def 5;
    then
A5: Y1 is bounded_above by RINFSUP1:5;
    (superior_realsequence (r (#) seq)).n
    = sup ((r (#) seq) ^\n) by RINFSUP1:39
      .= sup (r (#) (seq^\n)) by SEQM_3:44
      .= sup (r ** Y1) by INTEGRA2:17
      .= r * sup (seq ^\n) by A1,A5,INTEGRA2:13
      .= r * (superior_realsequence seq).n by RINFSUP1:39;
    hence (superior_realsequence (r (#) seq)).n
    = (r (#) (superior_realsequence seq)).n by SEQ_1:13;
  end;
  then superior_realsequence (r (#) seq)
  = r (#) (superior_realsequence seq) by FUNCT_2:113;
  then rng superior_realsequence (r (#) seq) = r ** X1 by INTEGRA2:17;
  hence thesis by A1,A3,INTEGRA2:15;
end;

registration
  let X be RealBanachSpace;
  cluster MetricSpaceNorm X -> complete;
  coherence
  proof
    now
      let S1 be sequence of MetricSpaceNorm X;
      assume
A1:   S1 is Cauchy;
      reconsider S2=S1 as sequence of X;
      S2 is Cauchy_sequence_by_Norm
      proof
        let r be Real;
        assume r > 0;
        then consider p be Element of NAT such that
A2:     for n,m be Element of NAT st p<=n & p<=m holds dist(S1.n,S1.m) < r
        by A1,TBSP_1:def 5;
        now
          let n,m be Element of 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 16;
      hence S1 is convergent by NORMSP_2:5;
    end;
    hence thesis by TBSP_1:def 6;
  end;
end;

definition
  let X be RealNormSpace, x0 be Point of X, r be real number;
  func Ball (x0,r) -> Subset of X equals
  { x where x is Point of X : ||.x0-x.|| < r };
  coherence
  proof
    defpred P[Point of X] means ||.x0 - $1.|| < r;
    {y where y is Point of X : P[y]} c= the carrier of X from FRAENKEL:sch 10;
    hence thesis;
  end;
end;

theorem Th3:

:: Baire category theorem - Banach space version
  for X be RealBanachSpace, Y be SetSequence of X st
  union rng Y = the carrier of X &
  (for n be Element of NAT holds Y.n is closed) holds
  ex n0 be Element of 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
A1: union rng Y = the carrier of X &
  for n be Element of NAT holds Y.n is closed;
  now
    let n be Element of NAT;
    reconsider Yn = Y.n as Subset of TopSpaceNorm X;
    Y.n is closed by A1;
    then Yn is closed by NORMSP_2:15;
    then Yn` is open by TOPS_1:29;
    hence (Y.n)` in Family_open_set MetricSpaceNorm X by PRE_TOPC:def 5;
  end;
  then consider n0 be Element of NAT, r be Real, xx0 be Point of
  MetricSpaceNorm X such that
A2: 0 < r & Ball(xx0,r) c= Y.n0 by A1,NORMSP_2:1;
  consider x0 be Point of X such that
A3: x0 = xx0 & Ball(xx0,r) = {x where x is Point of X:||.x0-x.|| < r}
  by NORMSP_2:2;
  Ball (x0,r) = {x where x is Point of X : ||.x0-x.|| < r };
  hence thesis by A2,A3;
end;

theorem Th4:
  for X,Y be RealNormSpace, f be bounded 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 bounded LinearOperator of X,Y;
A1: dom f =the carrier of X by FUNCT_2:def 1;
  consider K being Real such that
A2: 0 <= K & for x being VECTOR of X holds ||. f.x .|| <= K * ||. x .||
  by LOPBAN_1:def 9;
A3: now
    let x,y be Point of X;
    assume x in the carrier of X & y in the carrier of X;
    f/.x -f/.y =f.x +(-1)* f.y by RLVECT_1:29;
    then f/.x -f/.y = f.x + f.((-1)*y) by LOPBAN_1:def 6;
    then f/.x -f/.y = f.(x+(-1)*y) by LOPBAN_1:def 5;
    then
A4: f/.x -f/.y =f.(x+-y) by RLVECT_1:29;
    0<=||. x-y .|| by NORMSP_1:8;
    then ||.f/.x -f/.y .||<=K*||. x-y .||+||. x-y .|| by A2,A4,XREAL_1:40;
    hence ||. f/.x -f/.y .|| <= (K+1) * ||. x-y .||;
  end;
  0 < (K+1) by A2;
  hence f is_Lipschitzian_on the carrier of X by A1,A3,NFCONT_1:def 13;
  hence
A5: f is_continuous_on the carrier of X by NFCONT_1:52;
  hereby
    let x be Point of X;
    f|(the carrier of X) = f by FUNCT_2:40;
    hence f is_continuous_in x by A5,NFCONT_1:def 11;
  end;
end;

theorem 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 ex K be real number 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 number 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 ex KTx be real number 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 is bounded LinearOperator of X,Y :f in T};
A3: for x be Point of X ex y be Element of bool REAL st P[x,y]
    proof
      let x be Point of X;
      take y = {||. f.x .|| where f is bounded LinearOperator of X,Y :f in T};
      now
        let z be set;
        assume z in y;
        then ex f be bounded 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 the carrier 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 is bounded LinearOperator of X,Y :f in T};
A5: for x be Point of X holds Ta.x is non empty
    proof
      let x be Point of X;
A6:   Ta.x = {||. f.x .|| where f is bounded LinearOperator of X,Y :f in T}
      by A4;
      consider f0 be set such that
A7:   f0 in T by A2,XBOOLE_0:def 1;
      reconsider f0 as bounded LinearOperator of X,Y by A7,LOPBAN_1:def 10;
      ||. f0.x .|| in Ta.x by A6,A7;
      hence Ta.x is non empty;
    end;
    defpred P[Element of NAT,set] means
    $2={x where x is Point of X: Ta.x is bounded_above & sup(Ta.x) <= $1};
A8: for n be Element of NAT 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 is Point of X:
      Ta.x is bounded_above & sup(Ta.x) <= n};
      now
        let z be set;
        assume z in y;

then ex x be Point of X st z=x & Ta.x is bounded_above & sup(Ta.x) <= n;
        hence z in the carrier of X;
      end;
      hence thesis by TARSKI:def 3;
    end;
    ex Xn be Function of NAT,bool the carrier of X st
    for n be Element of NAT holds P[n,Xn.n] from FUNCT_2:sch 3(A8);
    then consider Xn be Function of NAT, bool the carrier of X such that
A9: for n be Element of NAT holds
    Xn.n = {x where x is Point of X: Ta.x is bounded_above & sup(Ta.x) <= n};
    reconsider Xn as SetSequence of X;
A10: for n be Element of NAT holds Xn.n is closed
    proof
      let n be Element of NAT;
      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
A11:    rng s1 c= Xn.n & s1 is convergent;
A12:    Ta.(lim s1) = {||. f.(lim s1) .||
        where f is bounded LinearOperator of X,Y :f in T} by A4;
A13:    for y be real number st y in Ta.(lim s1) holds y <= n
        proof
          let y be real number;
          assume y in Ta.(lim s1);
          then consider f be bounded LinearOperator of X,Y such that
A14:      y=||. f.(lim s1) .|| & f in T by A12;
A15:      f is_continuous_in lim s1 by Th4;
A16:      dom f=the carrier of X by FUNCT_2:def 1;
          then rng s1 c= dom f by A11,XBOOLE_1:1;
          then
A17:      f*s1 is convergent & f/.(lim s1) = lim (f*s1)
          by A11,A15,NFCONT_1:def 9;
          then
A18:      lim (||. f*s1 .||) = ||. f/.(lim s1) .|| by LOPBAN_1:24;
          for k be Element of NAT holds ||. f*s1 .||.k <= n
          proof
            let k be Element of NAT;
            ||. f*s1 .||.k = ||. (f*s1).k .|| by NORMSP_1:def 10;
            then
A19:        ||. f*s1 .||.k =||. f/.(s1.k) .|| by A11,A16,NFCONT_1:8,XBOOLE_1:1;
            dom s1= NAT by FUNCT_2:def 1;
            then s1.k in rng s1 by FUNCT_1:12;
            then s1.k in Xn.n by A11;
            then s1.k in {x where x is Point of X :
            Ta.x is bounded_above & sup (Ta.x) <= n} by A9;
            then consider x be Point of X such that
A20:        x=s1.k & Ta.x is bounded_above & sup(Ta.x) <=n;

Ta.x = {||. g.x .|| where g is bounded LinearOperator of X,Y :g in T} by A4;
            then ||. f.(s1.k) .|| in Ta.(s1.k) by A14,A20;
            then ||. f.(s1.k) .|| <= sup (Ta.(s1.k)) by A20,SEQ_4:def 4;
            hence thesis by A19,A20,XXREAL_0:2;
          end;
          then
A21:      for i being Element of NAT st 0 <= i holds ||. f*s1 .||.i <=n;
          ||. f*s1 .|| is convergent by A17,NORMSP_1:39;
          hence y<=n by A14,A18,A21,RSSPACE2:6;
        end;
        Ta.(lim s1) is non empty by A5;
        then
A22:    sup(Ta.(lim s1)) <= n by A13,SEQ_4:62;
A23:    Ta.(lim s1) is bounded_above by A13,SEQ_4:def 1;
        Xn.n = {x where x is Point of X :
        Ta.x is bounded_above & sup (Ta.x) <= n} by A9;
        hence thesis by A22,A23;
      end;
      hence thesis by NFCONT_1:def 5;
    end;
A24: union rng Xn is Subset of X by PROB_1:23;
    the carrier of X c= union rng Xn
    proof
      let x be set;
      assume x in the carrier of X;
      then reconsider x1=x as Point of X;
A25:  Ta.x1 = {||. f.x1 .|| where f is bounded LinearOperator of X,Y :f in T}
      by A4;
      consider f be set such that
A26:  f in T by A2,XBOOLE_0:def 1;
      reconsider f as bounded LinearOperator of X,Y by A26,LOPBAN_1:def 10;
A27:  ||. f.x1 .|| in Ta.x by A25,A26;
      consider KTx1 be real number such that
A28:  0 <= KTx1 &
      for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st
      f in T holds ||. f.x1 .|| <= KTx1 by A1;
A29:  for p be real number st p in Ta.x1 holds p <= KTx1
      proof
        let p be real number;
        assume p in Ta.x1;

then ex f be bounded LinearOperator of X,Y st p=||. f.x1 .|| & f in T by A25;
        hence p <= KTx1 by A28;
      end;
      then
A30:  Ta.x1 is bounded_above by SEQ_4:def 1;
      consider n be Element of NAT such that
A31:  KTx1 <n by SEQ_4:10;
      upper_bound (Ta.x1) <= KTx1 by A27,A29,SEQ_4:62;
      then upper_bound (Ta.x1) <= n by A31,XXREAL_0:2;
      then x1 in {z1 where z1 is Point of X :
      Ta.z1 is bounded_above & sup (Ta.z1) <= n} by A30;
      then x1 in Xn.n by A9;
      then x1 in Union Xn by PROB_1:25;
      hence x in union rng Xn;
    end;
    then union rng Xn = the carrier of X by A24,XBOOLE_0:def 10;
    then consider n0 be Element of NAT, r be Real,x0 be Point of X such that
A32: 0 < r & S0(x0,r) c= Xn.n0 by A10,Th3;
A33: for f be bounded LinearOperator of X,Y st f in T
    for x be Point of X st x in S0(x0,r) holds ||. f.x .|| <= n0
    proof
      let f be bounded LinearOperator of X,Y;
      assume
A34:  f in T;
      let x be Point of X;
      assume x in S0(x0,r);
      then x in Xn.n0 by A32;
      then x in {x1 where x1 is Point of X :
      Ta.x1 is bounded_above & sup (Ta.x1) <= n0} by A9;
      then consider x1 be Point of X such that
A35:  x1=x & Ta.x1 is bounded_above & sup(Ta.x1) <= n0;
      Ta.x1 = {||. g.x1 .||
      where g is bounded LinearOperator of X,Y :g in T} by A4;
      then ||. f.x .|| in Ta.x by A34,A35;
      then ||. f.x .|| <= sup (Ta.x) by A35,SEQ_4:def 4;
      hence ||. f.x .|| <= n0 by A35,XXREAL_0:2;
    end;
A36: 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;
      assume x <> 0.X;
      then
A37:  ||.x.|| <> 0 by NORMSP_1:def 2;
A38:  ||.x.|| >=0 by NORMSP_1:8;
A39:  abs( ||.x.||") =||.x.||" by A38,ABSVALUE:def 1;
A40:  0<r/2 by A32,XREAL_1:217;
      reconsider x1= (||.x.||")*x as Point of X;
      ||.x1.|| = abs( ||.x.||")*||.x.|| by NORMSP_1:def 2;
      then
A41:  ||.x1.|| = 1 by A37,A39,XCMPLX_0:def 7;
      ||.(r/2)*x1.|| = abs(r/2)*||.x1.|| by NORMSP_1:def 2;
      then
A42:  ||.(r/2)*x1.|| = r/2 by A40,A41,ABSVALUE:def 1;
A43:  r/2<r by A32,XREAL_1:218;
      ||. r/(2*||.x.||)*x+x0-x0.||
      =||.r/(2*||.x.||)*x+(x0+-x0).|| by RLVECT_1:def 6;
      then ||. r/(2*||.x.||)*x+x0-x0.||
      =||.r/(2*||.x.||)*x+0.X.|| by RLVECT_1:16;
      then ||. r/(2*||.x.||)*x+x0-x0.||
      =||.r/(2*||.x.||)*x.|| by RLVECT_1:def 7;
      then ||. r/(2*||.x.||)*x+x0-x0.|| =||.r/2/(||.x.||)*x.|| by XCMPLX_1:79;
      then ||. r/(2*||.x.||)*x+x0-x0.|| =||.(r/2)*x1.|| by RLVECT_1:def 9;
      then ||.x0-(r/(2*||.x.||)*x+x0).|| =r/2 by A42,NORMSP_1:11;
      hence r/(2*||.x.||)*x+x0 in S0(x0,r) by A43;
    end;
    set M=sup(Ta.x0);
    ||.x0-x0.||=||.0.X.|| by RLVECT_1:16;
    then x0 in S0(x0,r) by A32;
    then x0 in Xn.n0 by A32;
    then x0 in {x1 where x1 is Point of X :
    Ta.x1 is bounded_above & sup (Ta.x1) <= n0} by A9;
    then consider xx1 be Point of X such that
A44: xx1=x0 & Ta.xx1 is bounded_above & sup (Ta.xx1) <= n0;
    consider f be set such that
A45: f in T by A2,XBOOLE_0:def 1;
    reconsider f as bounded LinearOperator of X,Y by A45,LOPBAN_1:def 10;
    take KT=2*(M+n0)/r;
    Ta.xx1 = {||. g.xx1 .|| where g is bounded LinearOperator of X,Y :g in T }
    by A4;
    then ||. f.x0 .|| in Ta.x0 by A44,A45;
    then ||. f.x0 .|| <= sup(Ta.x0) by A44,SEQ_4:def 4;
    then 0<= sup (Ta.x0) by NORMSP_1:8;
    then (M+n0)>=0;
    then
A46: 2*(M+n0)>=0;
    then
A47: 0 <= KT by A32;
A48: now
      let f be bounded LinearOperator of X,Y;
      assume
A49:  f in T;
A50:  for x be Point of X st x <> 0.X holds ||.f.x.|| <= KT*||.x.||
      proof
        let x be Point of X;
        assume
A51:    x <> 0.X;
        then ||.x.|| <> 0 by NORMSP_1:def 2;
        then ||.x.|| >0 by NORMSP_1:8;
        then
A52:    2*||.x.|| >0 by XREAL_1:131;
        then
A53:    r/(2*||.x.||) >0 by A32,XREAL_1:141;
A54:    ||. f.(r/(2*||.x.||)*x+x0) .|| <= n0 by A33,A36,A49,A51;
A55:    (2*||.x.||)/r >0 by A32,A52,XREAL_1:141;
        set nrp1=r/(2*||.x.||);
        set nrp2=(2*||.x.||)/r;
        ||. f.(r/(2*||.x.||)*x).||
        =||.(r/(2*||.x.||))*f.x.|| by LOPBAN_1:def 6;
        then ||. f.(r/(2*||.x.||)*x).||
        =abs(r/(2*||.x.||))*||.f.x.|| by NORMSP_1:def 2;
        then
A56:    ||. f.(r/(2*||.x.||)*x).||
        =(r/(2*||.x.||))*||.f.x.|| by A53,ABSVALUE:def 1;
A57:    ||.f.(r/(2*||.x.||)*x)+f.x0.|| =||.f.(r/(2*||.x.||)*x+x0).||
        by LOPBAN_1:def 5;
        set nr1=||.f.(r/(2*||.x.||)*x)+f.x0.||;
        set nr2=||.f.(r/(2*||.x.||)*x).||;
        set nr3=||.f.x0.||;
        ||.-(f.x0).||=||.f.x0.|| by NORMSP_1:6;
        then nr2-nr3<=||.f.(r/(2*||.x.||)*x)-(-f.x0).|| by NORMSP_1:12;
        then (r/(2*||.x.||))*||.f.x.||-nr3<=nr1 by A56,RLVECT_1:30;
        then
A58:    (r/(2*||.x.||))*||.f.x.||-nr3<=n0 by A54,A57,XXREAL_0:2;
        ||.x0-x0.||=||.0.X.|| by RLVECT_1:16;
        then x0 in S0(x0,r) by A32;
        then x0 in Xn.n0 by A32;
        then x0 in {x1 where x1 is Point of X :
        Ta.x1 is bounded_above & sup(Ta.x1) <= n0} by A9;
        then consider x1 be Point of X such that
A59:    x1=x0 & Ta.x1 is bounded_above & sup (Ta.x1) <= n0;
        Ta.x1 = {||. g.x1 .|| where g is bounded LinearOperator of X,Y
        :g in T } by A4;
        then ||. f.x0 .|| in Ta.x0 by A49,A59;
        then ||. f.x0 .|| <= sup (Ta.x0) by A59,SEQ_4:def 4;
        then nrp1*||.f.x.|| - M <= nrp1*||.f.x.|| - nr3 by XREAL_1:12;
        then nrp1*||.f.x.|| - M <= n0 by A58,XXREAL_0:2;
        then nrp1*||.f.x.|| + -M + M <= n0 + M by XREAL_1:8;
        then nrp2*(nrp1*||.f.x.||) <= nrp2*(n0+M) by A55,XREAL_1:66;
        then nrp1*nrp2*||.f.x.|| <= nrp2*(n0+M);
        then 1*||.f.x.|| <= nrp2*(n0+M) by A32,A52,XCMPLX_1:113;
        hence ||.f.x.|| <= KT*||.x.||;
      end;
A60:  for x be Point of X holds ||.f.x.|| <= KT*||.x.||
      proof
        let x be Point of X;
        now
          assume
A61:      x = 0.X;
          then f.x = f.(0*0.X) by RLVECT_1:23;
          then f.x =0*f.(0.X) by LOPBAN_1:def 6;
          then
A62:      f.x =0.Y by RLVECT_1:23;
          ||.x.||= 0 by A61;
          hence ||.f.x.|| <= KT*||.x.|| by A62;
        end;
        hence thesis by A50;
      end; thus
      for k be real number st
      k in {||.f.x1.|| where x1 is Point of X : ||.x1.|| <= 1 } holds k <= KT
      proof
        let k be real number;
        assume k in {||.f.x1.|| where x1 is Point of X : ||.x1.|| <= 1};
        then consider x be Point of X such that
A63:    k=||.f.x.|| & ||.x.|| <= 1;
        k <= KT*||.x.|| & KT*||.x.|| <=KT by A47,A60,A63,XREAL_1:155;
        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 bounded LinearOperator of X,Y by LOPBAN_1:def 10;
      assume f in T;
      then
A64:  for k be real number st k in PreNorms(f1) holds k <= KT by A48;
      ||. f .|| = sup PreNorms(f1) by LOPBAN_1:36;
      hence ||. f .|| <= KT by A64,SEQ_4:62;
    end;
    hence thesis by A32,A46;
  end;
  suppose
A65: T = {};
    take L = 0;
    thus thesis by A65;
  end;
end;

definition
  let X, Y be RealNormSpace, H be Function of NAT,
  the carrier of R_NormSpace_of_BoundedLinearOperators(X,Y), x be Point of X;
  func H # x -> sequence of Y means
  :Def2:
  for n be Element of NAT holds it.n = (H.n).x;
  existence
  proof
    deffunc U(Element of NAT) = (H.$1).x;
    thus ex f being Function of NAT, the carrier of Y st
    for n be Element of NAT holds f.n = U(n) from FUNCT_2:sch 4;
  end;
  uniqueness
  proof
    let S1,S2 be sequence of Y such that
A1: (for n be Element of NAT holds S1.n = (H.n).x) &
    for n be Element of NAT holds S2.n = (H.n).x;
    now
      let n be Element of NAT;
      S1.n = (H.n).x & S2.n = (H.n).x by A1;
      hence S1.n = S2.n;
    end;
    hence thesis by FUNCT_2:113;
  end;
end;

theorem 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 bounded 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;
  assume
A1: for x be Point of X holds vseq#x is convergent & tseq.x = lim(vseq#x);
  set T=rng vseq;
  set RNS=R_NormSpace_of_BoundedLinearOperators(X,Y);
  vseq in Funcs(NAT,the carrier of RNS) by FUNCT_2:11;
  then consider f0 being Function such that
A2: vseq = f0 & dom f0 = NAT & rng f0 c= the carrier of RNS by FUNCT_2:def 2;
  for x be Point of X ex K be real number 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:39,SEQ_2:27;
    then ||. vseq#x .|| is bounded_above by SEQ_2:def 5;
    then consider K be real number such that
A3: for n be Element of NAT holds ||. vseq#x .||.n< K by SEQ_2:def 3;
    ||. vseq#x .||.0< K by A3;
    then ||. (vseq#x).0 .|| < K by NORMSP_1:def 10;
    then
A4: 0 <= K by NORMSP_1:8;
    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 set such that
A5:   n in NAT & f=vseq.n by FUNCT_2:17;
      reconsider n as Element of NAT by A5;
      (vseq.n).x = (vseq#x).n by Def2;
      then ||. f.x .|| = ||. vseq#x .||.n by A5,NORMSP_1:def 10;
      hence ||. f.x .|| <= K by A3;
    end;
    hence thesis by A4;
  end;
  then consider L be real number such that
A6: 0 <= L & for f be Point of RNS st f in T holds ||.f.|| <= L by A2,Th5;
A7: L + 0 < 1+ L by XREAL_1:10;
  for n be Element of NAT holds abs(||.vseq.||.n ) < (1+L)
  proof
    let n be Element of NAT;
    ||.vseq.n.|| <= L by A6,FUNCT_2:6;
    then ||.vseq.||.n <= L by NORMSP_1:def 10;
    then
A8: ||.vseq.||.n <(1+L) by A7,XXREAL_0:2;
    0<=||.vseq.n.|| by NORMSP_1:8;
    then 0<=||.vseq.||.n by NORMSP_1:def 10;
    hence thesis by A8,ABSVALUE:def 1;
  end;
  then
A9: ||.vseq.|| is bounded by A6,SEQ_2:15;
A10: for x,y be Point of X holds tseq.(x+y)= tseq.x + tseq.y
  proof
    let x,y be Point of X;
A11: (for n be Element of NAT holds (vseq.n).x = (vseq#x).n) &
    vseq#x is convergent & tseq.x = lim (vseq#x) by A1,Def2;
A12: (for n be Element of NAT holds (vseq.n).y = (vseq#y).n) &
    vseq#y is convergent & tseq.y = lim (vseq#y) by A1,Def2;
    now
      let n be Element of NAT;
A13:  (vseq.n).y = (vseq#y).n by Def2;
A14:  vseq.n is bounded LinearOperator of X,Y by LOPBAN_1:def 10;
      (vseq#(x+y)).n=(vseq.n).(x+y) by Def2;
      then (vseq#(x+y)).n=(vseq.n).x + (vseq.n).y by A14,LOPBAN_1:def 5;
      hence (vseq#(x+y)).n=(vseq#x).n + (vseq#y).n by A13,Def2;
    end;
    then
A15: vseq#(x+y) = vseq#x + vseq#y by NORMSP_1:def 5;
    tseq.(x+y) = lim (vseq#(x+y)) by A1;
    hence tseq.(x+y) = tseq.x + tseq.y by A11,A12,A15,NORMSP_1:42;
  end;
A16: for x be Point of X, r be Element of REAL holds tseq.(r*x)= r*tseq.x
  proof
    let x be Point of X, r be Element of REAL;
A17: (for n be Element of NAT holds (vseq.n).x = (vseq#x).n) &
    vseq#x is convergent & tseq.x = lim(vseq#x) by A1,Def2;
A18: now
      let n be Element of NAT;
A19:  vseq.n is bounded LinearOperator of X,Y by LOPBAN_1:def 10;
      (vseq#(r*x)).n=(vseq.n).(r*x) by Def2;
      then (vseq#(r*x)).n=r*(vseq.n).x by A19,LOPBAN_1:def 6;
      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 A18,NORMSP_1:def 8;
    hence tseq.(r*x) = r*tseq.x by A17,NORMSP_1:45;
  end;
A20: for x be Point of X holds ||.tseq.x.|| <=( lim_inf ||.vseq.|| ) * ||.x.||
  proof
    let x be Point of X;
A21: for n be Element of NAT holds ||.(vseq#x).n.|| <= ||.vseq.n.|| * ||.x.||
    proof
      let n be Element of NAT;
A22:  (vseq.n).x = (vseq#x).n by Def2;
      vseq.n is bounded LinearOperator of X,Y by LOPBAN_1:def 10;
      hence thesis by A22,LOPBAN_1:38;
    end;
A23: (for n be Element of NAT holds (vseq.n).x = (vseq#x).n) &
    vseq#x is convergent & tseq.x = lim(vseq#x) by A1,Def2;
    then
A24: ||. vseq#x .|| is convergent by LOPBAN_1:24;
    then
A25: ||. vseq#x .|| is bounded by SEQ_2:27;
A26: ||.x.|| (#) ||.vseq .|| is bounded by A9,SEQM_3:70;
A27: for n be Element of NAT holds
    ||. vseq#x .||.n <= (||.x.|| (#) ||.vseq .||).n
    proof
      let n be Element of NAT;
A28:  ||. vseq#x .||.n = ||.(vseq#x).n .|| by NORMSP_1:def 10;
A29:  ||.(vseq#x).n .|| <= ||.vseq.n.|| * ||.x.|| by A21;
      ||.vseq.n.|| = ||.vseq.||.n by NORMSP_1:def 10;
      hence thesis by A28,A29,SEQ_1:13;
    end;
A30: lim_inf (||.x.|| (#) ||.vseq .||)
    = ( lim_inf ||.vseq.|| ) * ||.x.|| by A9,Th1,NORMSP_1:8;
A31: lim ||. vseq#x .|| = lim_inf ||. vseq#x .|| by A24,RINFSUP1:91;
    lim_inf ||. vseq#x .|| <=lim_inf (||.x.|| (#) ||.vseq .||)
    by A25,A26,A27,RINFSUP1:93;
    hence thesis by A23,A30,A31,LOPBAN_1:24;
  end;
  now
    let s be real number;
    assume
A32: 0<s;
    for k be Element of NAT holds 0-s < ||.vseq.||.(0+k)
    proof
      let k be Element of NAT;
      ||.vseq.k.||=||.vseq.||.k by NORMSP_1:def 10;
      then 0<=||.vseq.||.k by NORMSP_1:8;
      hence thesis by A32;
    end;
    hence ex n be Element of NAT st
    for k be Element of NAT holds 0-s<||.vseq.||.(n+k);
  end;
  then
A33: 0 <= lim_inf||.vseq.|| by A9,RINFSUP1:84;
  then reconsider tseq1 = tseq as bounded LinearOperator of X,Y
  by A10,A16,A20,LOPBAN_1:def 5,def 6,def 9;
  for ttseq be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st
  ttseq = tseq holds ||.ttseq.|| <=( lim_inf ||.vseq.|| )
  proof
    let ttseq be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) such that
A34: ttseq=tseq;
    for k be real number st
    k in {||.tseq.x1.|| where x1 is Point of X : ||.x1.|| <= 1 } holds
    k <= ( lim_inf ||.vseq.|| )
    proof
      let k be real number;
      assume k in {||.tseq.x1.|| where x1 is Point of X : ||.x1.|| <= 1 };
      then consider x be Point of X such that
A35:  k=||.tseq.x.|| & ||.x.|| <= 1;
A36:  k <= (lim_inf ||.vseq.||) * ||.x.|| by A20,A35;
      (lim_inf ||.vseq.||) * ||.x.|| <= lim_inf ||.vseq.||
      by A33,A35,XREAL_1:155;
      hence thesis by A36,XXREAL_0:2;
    end;
    then sup PreNorms(tseq1) <=lim_inf ||.vseq.|| by SEQ_4:62;
    hence ||. ttseq .|| <= lim_inf ||.vseq.|| by A34,LOPBAN_1:36;
  end;
  hence thesis by A10,A16,A20,A33,LOPBAN_1:def 5,def 6,def 9;
end;

begin :: Banach-Steinhaus Principle

theorem 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 ex K be real number st
  0<=K & for n be Element of 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;
  assume
A2: for x be Point of X st x in X0 holds vseq#x is convergent;
  assume
A3: for x be Point of X ex K be real number st
  0<=K & for n be Element of NAT holds ||.(vseq#x).n.|| <=K;
  set T=rng vseq;
  vseq in Funcs(NAT,the carrier of R_NormSpace_of_BoundedLinearOperators(X,Y)
  ) by FUNCT_2:11;
  then consider f0 being Function such that
A4: vseq = f0 & dom f0 = NAT &
  rng f0 c= the carrier of R_NormSpace_of_BoundedLinearOperators(X,Y)
  by FUNCT_2:def 2;
  reconsider T as Subset of R_NormSpace_of_BoundedLinearOperators(X,Y) by A4;
  for x be Point of X ex K be real number 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 number such that
A5: 0<= K & for n be Element of 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 set such that
A6:   n in NAT & f=vseq.n by FUNCT_2:17;
      reconsider n as Element of NAT by A6;
      ||. f.x .|| = ||.(vseq#x).n.|| by A6,Def2;
      hence ||. f.x .|| <= K by A5;
    end;
    hence thesis by A5;
  end;
  then consider L be real number such that
A7: 0 <= L & for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st
  f in T holds ||.f.|| <= L by Th5;
  set M=1+L;
A8: L+0<M by XREAL_1:10;
A9: for f be bounded 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 bounded LinearOperator of X,Y;
    assume
A10: f in T;
    let x,y be Point of X;
    ||. f.x -f.y.|| = ||. f.x +(-1)*(f.y).|| by RLVECT_1:29;
    then ||. f.x -f.y.|| = ||. f.x +(f.((-1)*y)).|| by LOPBAN_1:def 6;
    then ||. f.x -f.y.|| = ||. f.(x +(-1)*y).|| by LOPBAN_1:def 5;
    then
A11: ||. f.x -f.y.|| = ||. f.(x -y).||by RLVECT_1:29;
    reconsider f1=f as Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
    by LOPBAN_1:def 10;
A12: ||. f.(x -y).|| <=||.f1.|| * ||.x-y.|| by LOPBAN_1:38;
    ||.f1.|| <= L by A7,A10;
    then
A13: ||.f1.|| < M by A8,XXREAL_0:2;
    0 <= ||.x-y.|| by NORMSP_1:8;
    then ||.f1.||* ||.x-y.|| <= M* ||.x-y.|| by A13,XREAL_1:66;
    hence ||. f.x -f.y.|| <=M* ||.x-y.|| by A11,A12,XXREAL_0:2;
  end;
  hereby
    let x be Point of X;
    for TK1 be Real st TK1 > 0 ex n0 be Element of NAT st
    for n,m be Element of NAT st n >= n0 & m >= n0 holds
    ||.(vseq#x).n -(vseq#x).m.||< TK1
    proof
      let TK1 be Real such that
A14:  TK1 > 0;
      set V = {z where z is Point of X : ||.x-z.|| <TK1/(3*M) };
      V c= the carrier of X
      proof
        let s be set;
        assume s in V;
        then ex z be Point of X st s=z & ||.x-z.|| <TK1/(3*M);
        hence s in the carrier of X;
      end;
      then reconsider V as Subset of LinearTopSpaceNorm(X) by NORMSP_2:def 4;
A15:  V is open by NORMSP_2:23;
      0 < (3*M) by A7,XREAL_1:131;
      then 0 < TK1/(3*M) by A14,XREAL_1:141;
      then ||.x-x.|| <TK1/(3*M) by NORMSP_1:10;
      then x in V;
      then X0 meets V by A1,A15,TOPS_1:80;
      then consider s be set such that
A16:  s in X0 & s in V by XBOOLE_0:3;
      consider y be Point of X such that
A17:  s=y & ||.x-y.|| < TK1/(3*M) by A16;
      vseq#y is convergent by A2,A16,A17;
      then for s be Real st 0<s ex n1 be Element of NAT st
      for m1 be Element of NAT st
      n1<=m1 holds ||.(vseq#y).m1 -(vseq#y).n1.||<s by LOPBAN_3:4;
      then
A18:  vseq#y is Cauchy_sequence_by_Norm by LOPBAN_3:5;
      0<TK1/3 by A14,XREAL_1:224;
      then consider n0 be Element of NAT such that
A19:  for n, m be Element of NAT st n >= n0 & m >= n0 holds
      ||.((vseq#y).n) - ((vseq#y).m).|| < TK1/3 by A18,RSSPACE3:10;
      take n0;
      for n, m be Element of NAT st n >= n0 & m >= n0 holds
      ||.(vseq#x).n -(vseq#x).m.||< TK1
      proof
        let n,m be Element of NAT;
        assume n >= n0 & m >= n0;
        then ||. (vseq#y).n - (vseq#y).m .|| < TK1/3 by A19;
        then ||. (vseq#x).n - (vseq#y).n .|| + ||. (vseq#y).n - (vseq#y).m .||
        < ||. (vseq#x).n - (vseq#y).n .||+ TK1/3 by XREAL_1:10;
        then
A20:    ||. (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:10;
        ||. (vseq#x).n - (vseq#y).m .|| <= ||. (vseq#x).n - (vseq#y).n .||
        + ||. (vseq#y).n - (vseq#y).m .|| by NORMSP_1:14;
        then
A21:    ||. (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:8;
        ||. (vseq#x).n - (vseq#x).m .|| <= ||. (vseq#x).n - (vseq#y).m .||
        + ||. (vseq#y).m - (vseq#x).m .|| by NORMSP_1:14;
        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 A21,XXREAL_0:2;
        then
A22:    ||. (vseq#x).n -(vseq#x).m .||
        < ||. (vseq#x).n - (vseq#y).n .||+ TK1/3
        + ||. (vseq#y).m - (vseq#x).m .|| by A20,XXREAL_0:2;
        reconsider f = vseq.n as bounded LinearOperator of X,Y
        by LOPBAN_1:def 10;
        ||. (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
A23:    ||. (vseq#x).n-(vseq#y).n .|| <= M*||.x-y.|| by A9,FUNCT_2:6;
        M*||.x-y.||<M* (TK1 / (3*M)) by A7,A17,XREAL_1:70;
        then M*||.x-y.||< TK1/3 by A7,XCMPLX_1:93;
        then ||. (vseq#x).n - (vseq#y).n.|| < TK1/3 by A23,XXREAL_0:2;
        then ||. (vseq#x).n-(vseq#y).n .||+ TK1/3 < TK1/3+TK1/3 by XREAL_1:10;
        then
A24:    ||. (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:10;

reconsider g =vseq.m as bounded LinearOperator of X,Y by LOPBAN_1:def 10;
        ||. (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 A9,FUNCT_2:6;
        M*||.x-y.||<M* (TK1 / (3*M)) by A7,A17,XREAL_1:70;
        then M*||.x-y.||< TK1/3 by A7,XCMPLX_1:93;
        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:11;
        then TK1/3 + TK1/3 + ||. (vseq#y).m-(vseq#x).m .||
        < TK1/3 + TK1/3 + TK1/3 by XREAL_1:10;
        then ||. (vseq#x).n-(vseq#y).n .|| + TK1/3 + ||. (vseq#y).m-(vseq#x).m
        .|| < TK1/3 + TK1/3 + TK1/3 by A24,XXREAL_0:2;
        hence thesis by A22,XXREAL_0:2;
      end;
      hence thesis;
    end;
    then vseq#x is Cauchy_sequence_by_Norm by RSSPACE3:10;
    hence vseq#x is convergent by LOPBAN_1:def 16;
  end;
end;

theorem
  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 ex K be real number st 0<=K &
  ( for n be Element of 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;
  assume
A2: for x be Point of X st x in X0 holds vseq#x is convergent;
  assume for x be Point of X ex K be real number st
  0<=K & for n be Element of NAT holds ||.(vseq#x).n.|| <= K;
  then
A3: for x be Point of X holds vseq#x is convergent by A1,A2,Th7;
  deffunc F(Point of X) = lim(vseq#$1);
  consider tseq be Function of X,Y such that
A4: for x be Point of X holds tseq.x=F(x) from FUNCT_2:sch 4;
  reconsider tseq as bounded LinearOperator of X,Y by A3,A4,Th6;
  reconsider tseq as Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
  by LOPBAN_1:def 10;
  take tseq;
  thus thesis by A3,A4,Th6;
end;