:: Inferior Limit and Superior Limit of Sequences of Real Numbers
::  by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received April 29, 2005
:: Copyright (c) 2005-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, SEQ_1, CARD_1, ARYTM_3, XXREAL_0, ARYTM_1,
      COMPLEX1, ORDINAL2, REAL_1, SEQ_4, RELAT_1, FUNCT_1, TARSKI, XXREAL_2,
      XBOOLE_0, SUPINF_2, PARTFUN3, NAT_1, VALUED_1, VALUED_0, SEQ_2, RINFSUP1,
      MEMBER_1;
 notations ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1,
      COMPLEX1, TARSKI, XXREAL_2, VALUED_0, FUNCT_1, SEQ_4, XBOOLE_0, SUBSET_1,
      COMSEQ_2, SEQ_2, RELSET_1, FUNCT_2, MEASURE6, VALUED_1, SEQ_1, PARTFUN3,
      MEMBER_1;
 constructors REAL_1, NAT_1, COMPLEX1, SEQM_3, LIMFUNC1, PARTFUN3, PARTFUN1,
      XXREAL_2, SEQ_4, RELSET_1, BINOP_2, SEQ_2, MEASURE6, MEMBER_1, SQUARE_1,
      COMSEQ_2;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED,
      VALUED_0, VALUED_1, FUNCT_2, SEQ_2, SEQ_4, RFUNCT_1, MEMBER_1, NAT_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, XBOOLE_0, PARTFUN3, XXREAL_2;
 equalities VALUED_1;
 expansions TARSKI, XBOOLE_0, PARTFUN3, VALUED_1, XXREAL_2;
 theorems FUNCT_1, FUNCT_2, SEQ_1, SEQ_2, NAT_1, TARSKI, XREAL_0, SEQ_4,
      SEQM_3, SETLIM_1, LIMFUNC1, PREPOWER, XREAL_1, XXREAL_0, ORDINAL1,
      RELAT_1, XXREAL_2, VALUED_0, MEASURE6, MEMBER_1;
 schemes FUNCT_2, NAT_1;

begin

reserve n,m,k,k1,k2 for Nat;
reserve r,r1,r2,s,t,p for Real;
reserve seq,seq1,seq2 for Real_Sequence;
reserve x,y for set;

Lm1: for s st 0 < s & r1 <= r2 holds r1 < r2 + s & r1 - s < r2
proof
  let s such that
A1: 0<s;
  assume r1 <= r2;
  then r1 + 0 < r2 + s by A1,XREAL_1:8;
  hence thesis by XREAL_1:19;
end;

theorem Th1:
  s - r < t & s + r > t iff |.t-s.| < r
proof
  thus s - r < t & s + r > t implies |.t-s.| < r
  proof
    assume that
A1: s - r < t and
A2: s + r > t;
    -r + s < t by A1;
    then
A3: -r < t - s by XREAL_1:20;
    t - s < r by A2,XREAL_1:19;
    hence thesis by A3,SEQ_2:1;
  end;
  assume
A4: |.t-s.| < r;
  then -r < t - s by SEQ_2:1;
  then
A5: s + -r < t by XREAL_1:20;
  t - s < r by A4,SEQ_2:1;
  hence thesis by A5,XREAL_1:19;
end;

definition
  let seq be Real_Sequence;
  func upper_bound seq -> Real equals
  upper_bound rng seq;
  coherence;
end;

definition
  let seq be Real_Sequence;
  func lower_bound seq -> Real equals
  lower_bound rng seq;
  coherence;
end;

theorem Th2:
  seq1+seq2-seq2=seq1
proof
  for n being Element of NAT holds (seq1+seq2-seq2).n = seq1.n
  proof
    let n be Element of NAT;
    (seq1+seq2-seq2).n = (seq1+(seq2-seq2)).n by SEQ_1:31
      .= seq1.n + (seq2+-seq2).n by SEQ_1:7
      .= seq1.n + (seq2.n +(-seq2).n) by SEQ_1:7
      .= seq1.n + (seq2.n +-seq2.n) by SEQ_1:10
      .= seq1.n;
    hence thesis;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th3:
  r in rng seq iff -r in rng(-seq)
proof
  thus r in rng seq implies -r in rng(-seq)
  proof
    assume r in rng seq;
    then consider n being Element of NAT such that
A1: r=seq.n by FUNCT_2:113;
    -r=(-seq).n by A1,SEQ_1:10;
    hence thesis by VALUED_0:28;
  end;
  assume -r in rng(-seq);
  then consider n being Element of NAT such that
A2: -r=(-seq).n by FUNCT_2:113;
  r=-(-seq).n by A2;
  then r= - -seq.n by SEQ_1:10;
  hence thesis by VALUED_0:28;
end;

theorem Th4:
  rng (-seq) = -- rng seq
proof
  thus rng (-seq) c= -- rng seq
  proof
    let x be object;
    assume
A1: x in rng(-seq);
    then reconsider r = x as Real;
    -r in rng -(-seq) by A1,Th3;
    then - -r in -- rng seq by MEASURE6:40;
    hence thesis;
  end;
  let x be object;
  assume
A2: x in -- rng seq;
  then reconsider r = x as Real;
  -r in -- -- rng seq by A2,MEMBER_1:12;
  then - -r in rng (-seq) by Th3;
  hence thesis;
end;

theorem Th5:
  seq is bounded_above iff rng seq is bounded_above
proof
A1: seq is bounded_above implies rng seq is bounded_above
  proof
    assume seq is bounded_above;
    then consider t such that
A2: for n holds seq.n<t by SEQ_2:def 3;
    t is UpperBound of rng seq
    proof
      let r be ExtReal;
      assume r in rng seq;
      then ex n being object st n in dom seq & seq.n = r by FUNCT_1:def 3;
      hence r<=t by A2;
    end;
    hence thesis;
  end;
  rng seq is bounded_above implies seq is bounded_above
  proof
    assume rng seq is bounded_above;
    then consider t such that
A3:  t is UpperBound of rng seq;
A4: for r st r in rng seq holds r<=t by A3,XXREAL_2:def 1;
    now
      let n;
A5:   n in NAT by ORDINAL1:def 12;
      seq.n <= t by A4,FUNCT_2:4,A5;
      hence seq.n < t+1 by Lm1;
    end;
    hence thesis by SEQ_2:def 3;
  end;
  hence thesis by A1;
end;

theorem Th6:
  seq is bounded_below iff rng seq is bounded_below
proof
A1: seq is bounded_below implies rng seq is bounded_below
  proof
    assume seq is bounded_below;
    then consider t such that
A2: for n holds t<seq.n by SEQ_2:def 4;
    t is LowerBound of rng seq
    proof
      let r be ExtReal;
      assume r in rng seq;
      then ex n being object st n in dom seq & seq.n = r by FUNCT_1:def 3;
      hence t<=r by A2;
    end;
    hence thesis;
  end;
  rng seq is bounded_below implies seq is bounded_below
  proof
    assume rng seq is bounded_below;
    then consider t such that
A3:  t is LowerBound of rng seq;
A4: for r st r in rng seq holds t<=r by A3,XXREAL_2:def 2;
    now
      let n;
A5:   n in NAT by ORDINAL1:def 12;
      t <= seq.n by A4,FUNCT_2:4,A5;
      hence t - 1 < seq.n by Lm1;
    end;
    hence thesis by SEQ_2:def 4;
  end;
  hence thesis by A1;
end;

theorem Th7:
  seq is bounded_above implies ( r = upper_bound seq iff (for n holds seq.n
  <= r) & for s st 0<s holds ex k st r-s < seq.k )
proof
  set R = rng seq;
  assume seq is bounded_above;
  then
A1: rng seq is bounded_above by Th5;
A2: rng seq <> {} by RELAT_1:41;
A3: (for n holds seq.n <= r) & (for s st 0<s holds ex k st r-s<seq.k)
  implies r = upper_bound seq
  proof
    assume that
A4: for n holds seq.n <= r and
A5: for s st 0<s holds ex k st r-s<seq.k;
A6: now
      let s;
      assume 0<s;
      then consider k such that
A7:   r-s< seq.k by A5;
A8:   k in NAT by ORDINAL1:def 12;
      consider r2 such that
A9:   r2 in R & r2 = seq.k by FUNCT_2:4,A8;
      take r2;
      thus r2 in R & r-s < r2 by A7,A9;
    end;
    now
      let r1;
      assume r1 in R;
      then ex n being object st n in dom seq & seq.n = r1 by FUNCT_1:def 3;
      hence r1 <= r by A4;
    end;
    hence thesis by A1,A2,A6,SEQ_4:def 1;
  end;
  r = upper_bound seq implies (for n holds seq.n <= r) &
  for s st 0<s holds ex k
  st r-s<seq.k
  proof
    assume
A10: r = upper_bound seq;
A11: now
      let s;
      assume 0<s;
      then consider r2 such that
A12:  r2 in R and
A13:  r-s<r2 by A1,A2,A10,SEQ_4:def 1;
      consider k being Nat such that
A14:  r2 = seq.k by A12,SETLIM_1:4;
       reconsider k as Nat;
      take k;
      thus r-s < seq.k by A13,A14;
    end;
    now
      let n;
A15:   n in NAT by ORDINAL1:def 12;
      seq.n in R by FUNCT_2:4,A15;
      hence seq.n <= r by A1,A10,SEQ_4:def 1;
    end;
    hence thesis by A11;
  end;
  hence thesis by A3;
end;

theorem Th8:
  seq is bounded_below implies (r = lower_bound seq iff (for n holds r <=
  seq.n) & for s st 0<s holds ex k st seq.k < r+s )
proof
  set R = rng seq;
  assume seq is bounded_below;
  then
A1: rng seq is bounded_below by Th6;
A2: rng seq <> {} by RELAT_1:41;
A3: (for n holds r <= seq.n) & (for s st 0<s holds ex k st seq.k<r+s)
  implies r = lower_bound seq
  proof
    assume that
A4: for n holds r <= seq.n and
A5: for s st 0<s holds ex k st seq.k<r+s;
A6: now
      let s;
      assume 0<s;
      then consider k such that
A7:   seq.k < r+s by A5;
A8:   k in NAT by ORDINAL1:def 12;
      consider r2 such that
A9:   r2 in R & r2 = seq.k by FUNCT_2:4,A8;
      take r2;
      thus r2 in R & r2 <r+s by A7,A9;
    end;
    now
      let r1;
      assume r1 in R;
      then ex n being object st n in dom seq & seq.n = r1 by FUNCT_1:def 3;
      hence r <= r1 by A4;
    end;
    hence thesis by A1,A2,A6,SEQ_4:def 2;
  end;
  r = lower_bound seq implies (for n holds r <= seq.n) &
  for s st 0<s holds ex k
  st seq.k<r+s
  proof
    assume
A10: r = lower_bound seq;
A11: now
      let s;
      assume 0<s;
      then consider r2 such that
A12:  r2 in R and
A13:  r2<r+s by A1,A2,A10,SEQ_4:def 2;
      consider k being Nat such that
A14:  r2 = seq.k by A12,SETLIM_1:4;
       reconsider k as Nat;
      take k;
      thus seq.k<r+s by A13,A14;
    end;
    now
      let n;
      n in NAT by ORDINAL1:def 12;
      then seq.n in R by FUNCT_2:4;
      hence r <= seq.n by A1,A10,SEQ_4:def 2;
    end;
    hence thesis by A11;
  end;
  hence thesis by A3;
end;

theorem Th9:
  (for n holds seq.n <= r) iff seq is bounded_above & upper_bound seq <= r
proof
  thus (for n holds seq.n <= r) implies seq is bounded_above &
  upper_bound seq <= r
  proof
    assume
A1: for n holds seq.n <= r;
    now
      let m;
      seq.m <= r by A1;
      hence seq.m < r + 1 by Lm1;
    end;
    hence
A2: seq is bounded_above by SEQ_2:def 3;
    now
      set r1= (upper_bound seq) - r;
      assume r < upper_bound seq;
      then r1 > 0 by XREAL_1:50;
      then ex k st (upper_bound seq) - r1 < seq.k by A2,Th7;
      hence contradiction by A1;
    end;
    hence thesis;
  end;
  assume that
A3: seq is bounded_above and
A4: upper_bound seq <= r;
  now
    let n;
    seq.n <= upper_bound seq by A3,Th7;
    hence seq.n <= r by A4,XXREAL_0:2;
  end;
  hence thesis;
end;

theorem Th10:
  (for n holds r <= seq.n) iff seq is bounded_below & r <= lower_bound seq
proof
  thus (for n holds r <= seq.n) implies seq is bounded_below &
  r <= lower_bound seq
  proof
    assume
A1: for n holds r <= seq.n;
    now
      let m;
      r <= seq.m by A1;
      hence r -1 < seq.m by Lm1;
    end;
    hence
A2: seq is bounded_below by SEQ_2:def 4;
    now
      set r1=r - (lower_bound seq);
      assume r > lower_bound seq;
      then r1 > 0 by XREAL_1:50;
      then ex k st seq.k < (lower_bound seq) + r1 by A2,Th8;
      hence contradiction by A1;
    end;
    hence thesis;
  end;
  assume that
A3: seq is bounded_below and
A4: r <= lower_bound seq;
  now
    let n;
    lower_bound seq <= seq.n by A3,Th8;
    hence r <= seq.n by A4,XXREAL_0:2;
  end;
  hence thesis;
end;

theorem
  seq is bounded_above iff -seq is bounded_below
proof
  set seq1=-seq;
  thus seq is bounded_above implies -seq is bounded_below;
  assume seq1 is bounded_below;
  then consider t such that
A1: for n holds seq1.n>t by SEQ_2:def 4;
  for n holds seq.n < -t
  proof
    let n;
    seq1.n=-seq.n by SEQ_1:10;
    then
A2: -seq1.n = seq.n;
    seq1.n > t by A1;
    hence thesis by A2,XREAL_1:24;
  end;
  hence thesis by SEQ_2:def 3;
end;

theorem
  seq is bounded_below iff -seq is bounded_above
proof
  - -seq = seq;
  hence thesis;
end;

theorem Th13:
  seq is bounded_above implies upper_bound seq = -lower_bound (-seq)
proof
  assume seq is bounded_above;
  then rng seq is non empty bounded_above by Th5,RELAT_1:41;
  then upper_bound rng seq = - lower_bound (--(rng seq)) by MEASURE6:44
    .= - lower_bound rng -seq by Th4;
  hence thesis;
end;

theorem Th14:
  seq is bounded_below implies lower_bound seq = -upper_bound (-seq)
proof
  assume seq is bounded_below;
  then rng seq is non empty bounded_below by Th6,RELAT_1:41;
  then lower_bound rng seq = - upper_bound --(rng seq) by MEASURE6:43
    .= - upper_bound rng -seq by Th4;
  hence thesis;
end;

theorem Th15:
  seq1 is bounded_below & seq2 is bounded_below implies lower_bound (seq1
  + seq2) >= lower_bound seq1 + lower_bound seq2
proof
  assume that
A1: seq1 is bounded_below and
A2: seq2 is bounded_below;
  for n holds (seq1 + seq2).n >= lower_bound seq1 + lower_bound seq2
  proof
    let n;
A3: seq2.n >= lower_bound seq2 by A2,Th8;
    (seq1 + seq2).n = seq1.n + seq2.n & seq1.n >= lower_bound seq1
    by A1,Th8,SEQ_1:7;
    hence thesis by A3,XREAL_1:7;
  end;
  hence thesis by Th10;
end;

theorem Th16:
  seq1 is bounded_above & seq2 is bounded_above implies upper_bound (seq1
  + seq2) <= upper_bound seq1 + upper_bound seq2
proof
  assume that
A1: seq1 is bounded_above and
A2: seq2 is bounded_above;
  for n holds (seq1 + seq2).n <= upper_bound seq1 + upper_bound seq2
  proof
    let n;
A3: seq2.n <= upper_bound seq2 by A2,Th7;
    (seq1 + seq2).n = seq1.n + seq2.n & seq1.n <= upper_bound seq1
    by A1,Th7,SEQ_1:7;
    hence thesis by A3,XREAL_1:7;
  end;
  hence thesis by Th9;
end;

notation
  let f be Real_Sequence;
  synonym f is nonnegative for f is nonnegative-yielding;
end;

definition
  let f be Real_Sequence;
  redefine attr f is nonnegative means
  for n holds f.n >= 0;
  compatibility
  proof
    thus f is nonnegative implies for n holds f.n >= 0 by VALUED_0:28;
    assume
A1: for n holds f.n >= 0;
    let r be Real;
    assume r in rng f;
    then ex x being Element of NAT st r = f.x by FUNCT_2:113;
    hence thesis by A1;
  end;
end;

theorem Th17:
  seq is nonnegative implies seq ^\k is nonnegative
proof
  assume
A1: seq is nonnegative;
  for n holds (seq ^\k).n >= 0
  proof
    let n;
    (seq ^\k).n = seq.(n+k) by NAT_1:def 3;
    hence thesis by A1;
  end;
  hence thesis;
end;

theorem Th18:
  seq is bounded_below nonnegative implies lower_bound seq >= 0
by Th10;

theorem
  seq is bounded_above nonnegative implies upper_bound seq >= 0
proof
  assume
A1: seq is bounded_above nonnegative;
  then
A2: seq.0 <= upper_bound seq by Th7;
  0 <= seq.0 by A1;
  hence thesis by A2;
end;

theorem Th20:
  seq1 is bounded_below nonnegative & seq2 is bounded_below
  nonnegative implies (seq1(#)seq2) is bounded_below &
  lower_bound (seq1 (#) seq2) >= (
  lower_bound seq1) * (lower_bound seq2)
proof
  assume that
A1: seq1 is bounded_below nonnegative and
A2: seq2 is bounded_below nonnegative;
  for n holds (seq1 (#) seq2).n >= (lower_bound seq1) * (lower_bound seq2)
  proof
    let n;
A3: (seq1 (#) seq2).n = seq1.n * seq2.n & seq1.n >=
lower_bound seq1 by A1,Th8,SEQ_1:8;
A4: lower_bound seq2 >= 0 by A2,Th18;
    seq2.n >= lower_bound seq2 & lower_bound seq1 >= 0 by A1,A2,Th8,Th18;
    hence thesis by A3,A4,XREAL_1:66;
  end;
  hence thesis by Th10;
end;

theorem Th21:
  seq1 is bounded_above nonnegative & seq2 is bounded_above
  nonnegative implies (seq1(#)seq2) is bounded_above &
  upper_bound (seq1 (#) seq2) <= (
  upper_bound seq1) * (upper_bound seq2)
proof
  assume that
A1: seq1 is bounded_above nonnegative and
A2: seq2 is bounded_above nonnegative;
  for n holds (seq1 (#) seq2).n <= (upper_bound seq1) * (upper_bound seq2)
  proof
    let n;
A3: (seq1 (#) seq2).n = seq1.n * seq2.n & seq1.n <= upper_bound seq1
by A1,Th7,SEQ_1:8;
A4: seq2.n >= 0 by A2;
    seq2.n <= upper_bound seq2 & seq1.n >= 0 by A1,A2,Th7;
    hence thesis by A3,A4,XREAL_1:66;
  end;
  hence thesis by Th9;
end;

theorem
  seq is non-decreasing bounded_above implies seq is bounded;

theorem
  seq is non-increasing bounded_below implies seq is bounded;

theorem Th24:
  seq is non-decreasing bounded_above implies lim seq = upper_bound seq
proof
  assume
A1: seq is non-decreasing bounded_above;
  then for n holds seq.n <= lim seq by SEQ_4:37;
  then
A2: upper_bound seq <= lim seq by Th9;
  for n holds seq.n <= upper_bound seq by A1,Th7;
  then lim seq <= upper_bound seq by A1,PREPOWER:2;
  hence thesis by A2,XXREAL_0:1;
end;

theorem Th25:
  seq is non-increasing bounded_below implies lim seq = lower_bound seq
proof
  assume
A1: seq is non-increasing bounded_below;
  then for n holds lim seq <= seq.n by SEQ_4:38;
  then
A2: lim seq <= lower_bound seq by Th10;
  for n holds lower_bound seq <= seq.n by A1,Th8;
  then lower_bound seq <= lim seq by A1,PREPOWER:1;
  hence thesis by A2,XXREAL_0:1;
end;

theorem
  seq is bounded_above implies seq ^\k is bounded_above by SEQM_3:27;

theorem
  seq is bounded_below implies seq ^\k is bounded_below by SEQM_3:28;

theorem
  seq is bounded implies seq ^\k is bounded by SEQM_3:29;

theorem Th29:
  for seq, n holds
    {seq.k: n <= k} is Subset of REAL
proof
  let seq, n;
  set Y = {seq.k: n <= k};
  now
    let x be object;
    assume x in Y;
    then consider z1 be set such that
A1: z1 = x and
A2: z1 in Y;
    consider k1 being Nat such that
A3: z1 = seq.k1 & n <= k1 by A2;
    reconsider k1 as Element of NAT by ORDINAL1:def 12;
    z1 = seq.k1 by A3;
    hence x in REAL by A1;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th30:
  rng (seq ^\ k) = {seq.n where n: k <= n}
proof
  set seq1 = seq ^\ k;
  set Z = {seq.m where m: k <= m};
  now
    let x be object;
    assume x in Z;
    then consider k1 being Nat such that
A1: x=seq.k1 and
A2: k <= k1;
    consider k2 being Nat such that
A3: k1 = k + k2 by A2,NAT_1:10;
    reconsider k2 as Element of NAT by ORDINAL1:def 12;
    x = seq1.k2 by A1,A3,NAT_1:def 3;
    hence x in rng seq1 by FUNCT_2:4;
  end;
  then
A4: Z c= rng seq1;
A5: dom seq1 = NAT by FUNCT_2:def 1;
  now
    let y be object;
    assume y in rng seq1;
    then consider m1 be object such that
A6: m1 in NAT and
A7: y = seq1.m1 by A5,FUNCT_1:def 3;
    reconsider m1 as Nat by A6;
    reconsider km1 = k+m1 as Nat;
    y = seq.(km1) by A7,NAT_1:def 3;
    hence y in Z by SETLIM_1:1;
  end;
  then rng seq1 c= Z;
  hence thesis by A4;
end;

theorem Th31:
  seq is bounded_above implies for n for R being Subset of REAL st
  R = {seq.k : n <= k} holds R is bounded_above
proof
  assume
A1: seq is bounded_above;
  let n;
  set seq1 = seq ^\n;
  seq1 is bounded_above by A1,SEQM_3:27;
  then
A2: rng seq1 is bounded_above by Th5;
  let R be Subset of REAL;
  assume R = {seq.k : n <= k};
  hence thesis by A2,Th30;
end;

theorem Th32:
  seq is bounded_below implies for n for R being Subset of REAL st
  R = {seq.k : n <= k} holds R is bounded_below
proof
  assume
A1: seq is bounded_below;
  let n;
  set seq1 = seq ^\n;
  seq1 is bounded_below by A1,SEQM_3:28;
  then
A2: rng seq1 is bounded_below by Th6;
  let R be Subset of REAL;
  assume R = {seq.k : n <= k};
  hence thesis by A2,Th30;
end;

theorem Th33:
  seq is bounded implies for n for R being Subset of REAL st R = {
  seq.k : n <= k} holds R is real-bounded
by Th31,Th32;

theorem Th34:
  seq is non-decreasing implies for n for R being Subset of REAL
  st R = {seq.k : n <= k} holds lower_bound R = seq.n
proof
  assume
A1: seq is non-decreasing;
  let n;
A2: now
    let r;
    assume r in {seq.k : n <= k};
    then consider r1 being Real such that
A3: r = r1 & r1 in {seq.k : n <= k};
    consider k1 such that
A4: r1 = seq.k1 and
A5: n <= k1 by A3;
    consider k being Nat such that
A6: n + k =k1 by A5,NAT_1:10;
    thus seq.n <= r by A1,A3,A4,A6,SEQM_3:5;
  end;
  let R be Subset of REAL;
A7: now
    let s;
A8: seq.n in {seq.k : n <= k};
    assume 0 < s;
    hence ex r st r in {seq.k : n <= k} & r< seq.n + s by A8,XREAL_1:29;
  end;
  assume
A9: R = {seq.k : n <= k};
  then
A10: R <> {} by SETLIM_1:1;
  R is bounded_below by A1,A9,Th32,LIMFUNC1:1;
  hence thesis by A9,A10,A2,A7,SEQ_4:def 2;
end;

theorem Th35:
  seq is non-increasing implies for n for R being Subset of REAL
  st R = {seq.k : n <= k} holds upper_bound R = seq.n
proof
  assume
A1: seq is non-increasing;
  let n;
A2: now
    let r;
    assume r in {seq.k : n <= k};
    then consider r1 being Real such that
A3: r = r1 & r1 in {seq.k : n <= k};
    consider k1 such that
A4: r1 = seq.k1 and
A5: n <= k1 by A3;
    consider k being Nat such that
A6: n + k =k1 by A5,NAT_1:10;
    thus r <= seq.n by A1,A3,A4,A6,SEQM_3:7;
  end;
  let R be Subset of REAL;
A7: now
    let s;
A8: seq.n in {seq.k : n <= k};
    assume 0 < s;
    hence ex r st r in {seq.k : n <= k} & seq.n - s < r by A8,XREAL_1:44;
  end;
  assume
A9: R = {seq.k : n <= k};
  then
A10: R <> {} by SETLIM_1:1;
  R is bounded_above by A1,A9,Th31,LIMFUNC1:1;
  hence thesis by A9,A10,A2,A7,SEQ_4:def 1;
end;

definition
  let seq be Real_Sequence;
  func inferior_realsequence seq -> Real_Sequence means
  :Def4:
  for n for Y being Subset of REAL st Y = {seq.k : n <= k}
    holds it.n = lower_bound Y;
  existence
proof
  defpred P[Element of NAT, Element of REAL] means for Y being Subset of REAL
  st Y = {seq.k: $1 <= k} holds $2 = lower_bound Y;
A1: for n being Element of NAT ex y being Element of REAL st P[n,y]
  proof
    let n be Element of NAT;
    reconsider Y={seq.k: n <= k} as Subset of REAL by Th29;
    reconsider y = lower_bound Y as Element of REAL by XREAL_0:def 1;
    for Y being Subset of REAL st Y = {seq.k: n <= k} holds y = lower_bound Y;
    hence thesis;
  end;
  consider f being sequence of REAL such that
A2:  for n being Element of NAT holds P[n,f.n] from FUNCT_2:sch 3(A1);
  take f;
  let n be Nat;
   n in NAT by ORDINAL1:def 12;
  hence thesis by A2;
end;
  uniqueness
  proof
    let seq1,seq2 be Real_Sequence such that
A3: for n for Y being Subset of REAL st Y = {seq.k : n <= k} holds
    seq1.n = lower_bound Y and
A4: for m for Y being Subset of REAL st Y = {seq.k : m <= k} holds
    seq2.m = lower_bound Y;
A5: for y being object st y in NAT holds seq1.y = seq2.y
    proof
      let y be object;
      assume y in NAT;
      then reconsider y as Element of NAT;
      reconsider Y = {seq.k: y <= k} as Subset of REAL by Th29;
      seq1.y = lower_bound Y by A3;
      hence thesis by A4;
    end;
    NAT = dom seq1 & NAT = dom seq2 by FUNCT_2:def 1;
    hence thesis by A5,FUNCT_1:2;
  end;
end;

definition
  let seq be Real_Sequence;
  func superior_realsequence seq -> Real_Sequence means
  :Def5:
  for n for Y
  being Subset of REAL st Y = {seq.k : n <= k} holds it.n = upper_bound Y;
  existence
proof
  defpred P[Element of NAT, Element of REAL] means for Y being Subset of REAL
  st Y = {seq.k: $1 <= k} holds $2 = upper_bound Y;
A1: for n being Element of NAT ex y being Element of REAL st P[n,y]
  proof
    let n be Element of NAT;
    reconsider Y={seq.k: n <= k} as Subset of REAL by Th29;
    reconsider y = upper_bound Y as Element of REAL by XREAL_0:def 1;
    for Y being Subset of REAL st Y = {seq.k: n <= k} holds y = upper_bound Y;
    hence thesis;
  end;
  consider f being sequence of REAL such that
A2:  for n being Element of NAT holds P[n,
  f.n] from FUNCT_2:sch 3(A1);
  take f;
  let n be Nat;
   n in NAT by ORDINAL1:def 12;
  hence thesis by A2;
end;
  uniqueness
  proof
    let seq1,seq2 be Real_Sequence such that
A3: for n for Y being Subset of REAL st Y = {seq.k : n <= k} holds
    seq1.n = upper_bound Y and
A4: for m for Y being Subset of REAL st Y = {seq.k : m <= k} holds
    seq2.m = upper_bound Y;
A5: for y being object st y in NAT holds seq1.y = seq2.y
    proof
      let y be object;
      assume y in NAT;
      then reconsider y as Element of NAT;
      reconsider Y = {seq.k: y <= k} as Subset of REAL by Th29;
      seq1.y = upper_bound Y by A3;
      hence thesis by A4;
    end;
    NAT = dom seq1 & NAT = dom seq2 by FUNCT_2:def 1;
    hence thesis by A5,FUNCT_1:2;
  end;
end;

theorem Th36:
  (inferior_realsequence seq).n = lower_bound (seq ^\n)
proof
  reconsider Y = {seq.k: n <= k} as Subset of REAL by Th29;
  (inferior_realsequence seq).n = lower_bound Y by Def4
    .= lower_bound rng (seq ^\ n) by Th30;
  hence thesis;
end;

theorem Th37:
  (superior_realsequence seq).n = upper_bound (seq ^\n)
proof
  reconsider Y = {seq.k: n <= k} as Subset of REAL by Th29;
  (superior_realsequence seq).n = upper_bound Y by Def5
    .= upper_bound rng (seq ^\ n) by Th30;
  hence thesis;
end;

theorem Th38:
  seq is bounded_below implies (inferior_realsequence seq).0 = lower_bound seq
proof
  reconsider Y1 = {seq.k : 0 <= k} as Subset of REAL by Th29;
  (inferior_realsequence seq).0 = lower_bound Y1 by Def4
    .= lower_bound seq by SETLIM_1:5;
  hence thesis;
end;

theorem Th39:
  seq is bounded_above implies (superior_realsequence seq).0 = upper_bound seq
proof
  reconsider Y1 = {seq.k : 0 <= k} as Subset of REAL by Th29;
  (superior_realsequence seq).0 = upper_bound Y1 by Def5
    .= upper_bound seq by SETLIM_1:5;
  hence thesis;
end;

theorem Th40:
  seq is bounded_below implies (r = (inferior_realsequence seq).n
  iff (for k holds r <= seq.(n+k)) & for s st 0<s ex k st seq.(n+k)<r+s)
proof
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  assume seq is bounded_below;
  then
A1: Y1 is non empty bounded_below by Th32,SETLIM_1:1;
  thus r = (inferior_realsequence seq).n implies (for k holds r<=seq.(n+k)) &
  for s st 0<s ex k st seq.(n+k)<r+s
  proof
    assume r = (inferior_realsequence seq).n;
    then
A2: r = lower_bound Y1 by Def4;
A3: for s st 0<s ex k st seq.(n+k)<r+s
    proof
      let s;
      assume 0<s;
      then consider r1 such that
A4:   r1 in Y1 and
A5:   r1<r+s by A1,A2,SEQ_4:def 2;
      consider k1 such that
A6:   r1=seq.k1 and
A7:   n <= k1 by A4;
      consider k2 being Nat such that
A8:   k1 = n + k2 by A7,NAT_1:10;
      thus thesis by A5,A6,A8;
    end;
    for k holds r<=seq.(n+k)
    proof
      let k;
      seq.(n+k) in Y1 by SETLIM_1:1;
      hence thesis by A1,A2,SEQ_4:def 2;
    end;
    hence thesis by A3;
  end;
  assume that
A9: for k holds r <= seq.(n+k) and
A10: for s st 0<s ex k st seq.(n+k)<r+s;
A11: for s st 0<s ex r1 st r1 in Y1 & r1<r+s
  proof
    let s;
    assume 0<s;
    then consider k such that
A12: seq.(n+k)<r+s by A10;
    n + k >= n by NAT_1:11;
    then seq.(n+k) in Y1;
    hence thesis by A12;
  end;
  for r1 st r1 in Y1 holds r <= r1
  proof
    let r1;
    assume r1 in Y1;
    then consider k1 such that
A13: r1=seq.k1 and
A14: n <= k1;
    consider k2 being Nat such that
A15: k1 = n + k2 by A14,NAT_1:10;
    thus thesis by A9,A13,A15;
  end;
  then r=lower_bound Y1 by A1,A11,SEQ_4:def 2;
  hence thesis by Def4;
end;

theorem Th41:
  seq is bounded_above implies (r = (superior_realsequence seq).n
  iff (for k holds seq.(n+k) <= r) & for s st 0<s ex k st r-s<seq.(n+k))
proof
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  assume seq is bounded_above;
  then
A1: Y1 is non empty bounded_above by Th31,SETLIM_1:1;
  thus r = (superior_realsequence seq).n implies (for k holds seq.(n+k) <= r)
  & for s st 0<s ex k st r-s<seq.(n+k)
  proof
    assume r = (superior_realsequence seq).n;
    then
A2: r = upper_bound Y1 by Def5;
A3: for s st 0<s ex k st r-s<seq.(n+k)
    proof
      let s;
      assume 0<s;
      then consider r1 such that
A4:   r1 in Y1 and
A5:   r-s<r1 by A1,A2,SEQ_4:def 1;
      consider k1 such that
A6:   r1=seq.k1 and
A7:   n <= k1 by A4;
      consider k2 being Nat such that
A8:   k1 = n + k2 by A7,NAT_1:10;
      thus thesis by A5,A6,A8;
    end;
    for k holds seq.(n+k) <= r
    proof
      let k;
      seq.(n+k) in Y1 by SETLIM_1:1;
      hence thesis by A1,A2,SEQ_4:def 1;
    end;
    hence thesis by A3;
  end;
  assume that
A9: for k holds seq.(n+k) <= r and
A10: for s st 0<s ex k st r-s<seq.(n+k);
A11: for s st 0<s ex r1 st r1 in Y1 & r-s<r1
  proof
    let s;
    assume 0<s;
    then consider k such that
A12: r-s<seq.(n+k) by A10;
    n + k >= n by NAT_1:11;
    then seq.(n+k) in Y1;
    hence thesis by A12;
  end;
  for r1 st r1 in Y1 holds r1 <= r
  proof
    let r1;
    assume r1 in Y1;
    then consider k1 such that
A13: r1=seq.k1 and
A14: n <= k1;
    consider k2 being Nat such that
A15: k1 = n + k2 by A14,NAT_1:10;
    thus thesis by A9,A13,A15;
  end;
  then r=upper_bound Y1 by A1,A11,SEQ_4:def 1;
  hence thesis by Def5;
end;

theorem Th42:
  seq is bounded_below implies ((for k holds r <= seq.(n+k)) iff r
  <= (inferior_realsequence seq).n)
proof
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  set seq1 = seq ^\n;
  assume seq is bounded_below;
  then
A1: seq1 is bounded_below by SEQM_3:28;
A2: rng seq1 = Y1 by Th30;
  thus (for k holds r <= seq.(n+k)) implies r <= (inferior_realsequence seq).n
  proof
    assume
A3: for k holds r <= seq.(n+k);
    now
      let n1 being Nat;
      n1 in NAT by ORDINAL1:def 12;
      then seq1.n1 in rng seq1 by FUNCT_2:4;
      then consider r1 such that
A4:   seq1.n1= r1 and
A5:   r1 in Y1 by A2;
      consider k1 being Nat such that
A6:   r1 = seq.k1 and
A7:   n <= k1 by A5;
      consider k2 being Nat such that
A8:   k1 = n + k2 by A7,NAT_1:10;
      thus r <= seq1.n1 by A3,A4,A6,A8;
    end;
    then r <= lower_bound seq1 by Th10;
    then r <= lower_bound Y1 by Th30;
    hence thesis by Def4;
  end;
  assume r <= (inferior_realsequence seq).n;
  then r <= lower_bound Y1 by Def4;
  then
A9: r <= lower_bound seq1 by Th30;
  now
    let m1 be Nat;
    n <= n+m1 by NAT_1:11;
    then seq.(n+m1) in Y1;
    then seq.(n+m1) in rng seq1 by Th30;
    then ex k being object st k in dom seq1 & seq1.k = seq.(n+m1)
by FUNCT_1:def 3;
    hence r <= seq.(n+m1) by A1,A9,Th10;
  end;
  hence thesis;
end;

theorem Th43:
  seq is bounded_below implies ((for m st n <= m holds r <= seq.m)
  iff r <= (inferior_realsequence seq).n)
proof
  assume
A1: seq is bounded_below;
  thus (for m st n<=m holds r <= seq.m) implies r <= (inferior_realsequence
  seq).n
  proof
    assume for m st n<=m holds r <= seq.m;
    then for k holds r <= seq.(n+k) by NAT_1:11;
    hence thesis by A1,Th42;
  end;
  assume
A2: r <= (inferior_realsequence seq).n;
  now
    let m;
    assume n<=m;
    then consider k being Nat such that
A3: m = n + k by NAT_1:10;
    thus r <= seq.m by A1,A2,A3,Th42;
  end;
  hence thesis;
end;

theorem Th44:
  seq is bounded_above implies ((for k holds seq.(n+k) <= r) iff (
  superior_realsequence seq).n <= r)
proof
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  set seq1 = seq ^\n;
  assume seq is bounded_above;
  then
A1: seq1 is bounded_above by SEQM_3:27;
A2: rng seq1 = Y1 by Th30;
  thus (for k holds seq.(n+k) <= r) implies (superior_realsequence seq).n <= r
  proof
    assume
A3: for k holds seq.(n+k) <= r;
    now
      let n1 being Nat;
      n1 in NAT by ORDINAL1:def 12;
      then seq1.n1 in rng seq1 by FUNCT_2:4;
      then consider r1 such that
A4:   seq1.n1= r1 and
A5:   r1 in Y1 by A2;
      consider k1 being Nat such that
A6:   r1 = seq.k1 and
A7:   n <= k1 by A5;
      consider k2 being Nat such that
A8:   k1 = n + k2 by A7,NAT_1:10;
      thus seq1.n1 <= r by A3,A4,A6,A8;
    end;
    then upper_bound seq1 <= r by Th9;
    then upper_bound Y1 <= r by Th30;
    hence thesis by Def5;
  end;
  assume (superior_realsequence seq).n <= r;
  then upper_bound Y1 <= r by Def5;
  then
A9: upper_bound seq1 <= r by Th30;
  now
    let m1 being Nat;
    n <= n+m1 by NAT_1:11;
    then seq.(n+m1) in Y1;
    then seq.(n+m1) in rng seq1 by Th30;
    then ex k being object st k in dom seq1 & seq1.k = seq.(n+m1)
by FUNCT_1:def 3;
    hence seq.(n+m1) <= r by A1,A9,Th9;
  end;
  hence thesis;
end;

theorem Th45:
  seq is bounded_above implies ((for m st n<=m holds seq.m <= r)
  iff (superior_realsequence seq).n <= r)
proof
  assume
A1: seq is bounded_above;
  thus (for m st n<=m holds seq.m <= r) implies (superior_realsequence seq).n
  <= r
  proof
    assume for m st n<=m holds seq.m <= r;
    then for k holds seq.(n+k) <= r by NAT_1:11;
    hence thesis by A1,Th44;
  end;
  assume
A2: (superior_realsequence seq).n <= r;
  now
    let m;
    assume n<=m;
    then consider k being Nat such that
A3: m = n + k by NAT_1:10;
    thus seq.m <= r by A1,A2,A3,Th44;
  end;
  hence thesis;
end;

theorem Th46:
  seq is bounded_below implies (inferior_realsequence seq).n = min
  ((inferior_realsequence seq).(n+1),seq.n)
proof
  reconsider Y2 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  reconsider Y3 = {seq.n} as Subset of REAL;
A1: (inferior_realsequence seq).(n+1) = lower_bound Y2 by Def4;
  assume
A2: seq is bounded_below;
  then
A3: Y2 <> {} & Y2 is bounded_below by Th32,SETLIM_1:1;
A4: Y3 is bounded_below
  proof
    consider t such that
A5: for m holds t<seq.m by A2,SEQ_2:def 4;
    t is LowerBound of Y3
    proof
      let r be ExtReal;
      assume r in Y3;
      then r = seq.n by TARSKI:def 1;
      hence t <= r by A5;
    end;
    hence thesis;
  end;
  (inferior_realsequence seq).n = lower_bound Y1 by Def4;
  then (inferior_realsequence seq).n = lower_bound (Y2 \/ Y3) by SETLIM_1:2
    .= min(lower_bound Y2,lower_bound Y3) by A3,A4,SEQ_4:142
    .= min((inferior_realsequence seq).(n+1),seq.n) by A1,SEQ_4:9;
  hence thesis;
end;

theorem Th47:
  seq is bounded_above implies (superior_realsequence seq).n = max
  ((superior_realsequence seq).(n+1),seq.n)
proof
  reconsider Y2 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  reconsider Y3 = {seq.n} as Subset of REAL;
A1: (superior_realsequence seq).(n+1) = upper_bound Y2 by Def5;
  assume
A2: seq is bounded_above;
  then
A3: Y2 <> {} & Y2 is bounded_above by Th31,SETLIM_1:1;
A4: Y3 is bounded_above
  proof
    consider t such that
A5: for m holds seq.m<t by A2,SEQ_2:def 3;
    t is UpperBound of Y3
    proof
      let r be ExtReal;
      assume r in Y3;
      then r = seq.n by TARSKI:def 1;
      hence r <=t by A5;
    end;
    hence thesis;
  end;
  (superior_realsequence seq).n = upper_bound Y1 by Def5;
  then (superior_realsequence seq).n = upper_bound (Y2 \/ Y3) by SETLIM_1:2
    .= max(upper_bound Y2,upper_bound Y3) by A3,A4,SEQ_4:143
    .= max((superior_realsequence seq).(n+1),seq.n) by A1,SEQ_4:9;
  hence thesis;
end;

theorem Th48:
  seq is bounded_below implies (inferior_realsequence seq).n <= (
  inferior_realsequence seq).(n+1)
proof
A1: min((inferior_realsequence seq).(n+1),seq.n) <= (inferior_realsequence
  seq).(n+1) by XXREAL_0:17;
  assume seq is bounded_below;
  hence thesis by A1,Th46;
end;

theorem Th49:
  seq is bounded_above implies (superior_realsequence seq).(n+1)
  <= (superior_realsequence seq).n
proof
A1: (superior_realsequence seq).(n+1) <= max((superior_realsequence seq).(n+
  1),seq.n) by XXREAL_0:25;
  assume seq is bounded_above;
  hence thesis by A1,Th47;
end;

theorem Th50:
  seq is bounded_below implies inferior_realsequence seq is non-decreasing
by Th48;

theorem Th51:
  seq is bounded_above implies superior_realsequence seq is non-increasing
by Th49;

theorem
  seq is bounded implies (inferior_realsequence seq).n <= (
  superior_realsequence seq).n
proof
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  assume
A1: seq is bounded;
A2: Y1 <> {} by SETLIM_1:1;
  (superior_realsequence seq).n = upper_bound Y1 &
  (inferior_realsequence seq).n =
  lower_bound Y1 by Def4,Def5;
  hence thesis by A1,A2,Th33,SEQ_4:11;
end;

theorem Th53:
  seq is bounded implies (inferior_realsequence seq).n <= lower_bound (
  superior_realsequence seq)
proof
  reconsider Y2 = {seq.k2 : n <= k2} as Subset of REAL by Th29;
  assume
A1: seq is bounded;
A2: now
    let m;
    reconsider Y1 = {seq.k1 : m <= k1} as Subset of REAL by Th29;
    n <= n + m by NAT_1:11;
    then
A3: seq.(n+m) in Y2;
    Y2 is real-bounded by A1,Th33;
    then Y2 is bounded_below;
    then
A4: lower_bound Y2 <= seq.(n+m) by A3,SEQ_4:def 2;
    m <= n + m by NAT_1:11;
    then
A5: seq.(n+m) in Y1;
    Y1 is real-bounded by A1,Th33;
    then Y1 is bounded_above;
    then
A6: seq.(n+m) <= upper_bound Y1 by A5,SEQ_4:def 1;
    (superior_realsequence seq).m = upper_bound Y1 by Def5;
    hence lower_bound Y2 <= (superior_realsequence seq).m by A6,A4,XXREAL_0:2;
  end;
  (inferior_realsequence seq).n = lower_bound Y2 by Def4;
  hence thesis by A2,Th10;
end;

theorem Th54:
  seq is bounded implies upper_bound(inferior_realsequence seq) <= (
  superior_realsequence seq).n
proof
  reconsider Y2 = {seq.k2 : n <= k2} as Subset of REAL by Th29;
  assume
A1: seq is bounded;
A2: now
    let m;
    reconsider Y1 = {seq.k1 : m <= k1} as Subset of REAL by Th29;
    n <= n + m by NAT_1:11;
    then
A3: seq.(n+m) in Y2;
    Y2 is real-bounded by A1,Th33;
    then Y2 is bounded_above;
    then
A4: upper_bound Y2 >= seq.(n+m) by A3,SEQ_4:def 1;
    m <= n + m by NAT_1:11;
    then
A5: seq.(n+m) in Y1;
    Y1 is real-bounded by A1,Th33;
    then Y1 is bounded_below;
    then
A6: seq.(n+m) >= lower_bound Y1 by A5,SEQ_4:def 2;
    (inferior_realsequence seq).m = lower_bound Y1 by Def4;
    hence upper_bound Y2 >= (inferior_realsequence seq).m by A6,A4,XXREAL_0:2;
  end;
  (superior_realsequence seq).n = upper_bound Y2 by Def5;
  hence thesis by A2,Th9;
end;

theorem Th55:
  seq is bounded implies upper_bound(inferior_realsequence seq) <= lower_bound(
  superior_realsequence seq)
proof
  set seq1 = (inferior_realsequence seq);
  set r = lower_bound(superior_realsequence seq);
  assume seq is bounded;
  then seq1.n <= r by Th53;
  hence thesis by Th9;
end;

theorem Th56:
  seq is bounded implies superior_realsequence seq is bounded &
  inferior_realsequence seq is bounded
proof
  assume
A1: seq is bounded;
  then inferior_realsequence seq is non-decreasing by Th50;
  then
A2: inferior_realsequence seq is bounded_below by LIMFUNC1:1;
  now
    let m;
    upper_bound(inferior_realsequence seq) <= (superior_realsequence seq).m
    by A1,Th54;
    hence (upper_bound(inferior_realsequence seq)) - 1 <
    (superior_realsequence seq).m
    by Lm1;
  end;
  then
A3: (superior_realsequence seq) is bounded_below by SEQ_2:def 4;
  now
    let m;
    (inferior_realsequence seq).m <= lower_bound (superior_realsequence seq)
    by A1,Th53;
    hence (inferior_realsequence seq).m <
    (lower_bound (superior_realsequence seq)) +1
    by Lm1;
  end;
  then
A4: (inferior_realsequence seq) is bounded_above by SEQ_2:def 3;
  superior_realsequence seq is non-increasing by A1,Th51;
  then superior_realsequence seq is bounded_above by LIMFUNC1:1;
  hence thesis by A2,A4,A3;
end;

theorem Th57:
  seq is bounded implies inferior_realsequence seq is convergent &
  lim inferior_realsequence seq = upper_bound inferior_realsequence seq
proof
  assume seq is bounded;
  then
  inferior_realsequence seq is non-decreasing & inferior_realsequence seq
  is bounded by Th50,Th56;
  hence thesis by Th24;
end;

theorem Th58:
  seq is bounded implies superior_realsequence seq is convergent &
  lim superior_realsequence seq = lower_bound superior_realsequence seq
proof
  assume seq is bounded;
  then
  superior_realsequence seq is non-increasing & superior_realsequence seq
  is bounded by Th51,Th56;
  hence thesis by Th25;
end;

theorem Th59:
  seq is bounded_below implies (inferior_realsequence seq).n = - (
  superior_realsequence(-seq)).n
proof
  assume
A1: seq is bounded_below;
  (inferior_realsequence seq).n = lower_bound (seq ^\n) by Th36
    .= - upper_bound -(seq ^\n) by A1,Th14,SEQM_3:28
    .= - upper_bound ((-seq) ^\n) by SEQM_3:16;
  hence thesis by Th37;
end;

theorem Th60:
  seq is bounded_above implies (superior_realsequence seq).n = - (
  inferior_realsequence(-seq)).n
proof
  assume
A1: seq is bounded_above;
  (superior_realsequence seq).n = upper_bound (seq ^\n) by Th37
    .= - lower_bound -(seq ^\n) by A1,Th13,SEQM_3:27
    .= - lower_bound ((-seq) ^\n) by SEQM_3:16;
  hence thesis by Th36;
end;

theorem Th61:
  seq is bounded_below implies (inferior_realsequence seq) = - (
  superior_realsequence(-seq))
proof
  assume seq is bounded_below;
  then (inferior_realsequence seq).n = - (superior_realsequence(-seq)).n by
Th59;
  hence thesis by SEQ_1:10;
end;

theorem Th62:
  seq is bounded_above implies (superior_realsequence seq) = - (
  inferior_realsequence(-seq))
proof
  assume seq is bounded_above;
  then (superior_realsequence seq).n = - (inferior_realsequence(-seq)).n by
Th60;
  hence thesis by SEQ_1:10;
end;

theorem
  seq is non-decreasing implies seq.n <= (inferior_realsequence seq).(n+ 1)
proof
  reconsider Y1 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
A1: (inferior_realsequence seq).(n+1) = lower_bound Y1 by Def4;
  assume
A2: seq is non-decreasing;
  then lower_bound Y1 = seq.(n+1) by Th34;
  hence thesis by A2,A1;
end;

Lm2: seq is non-decreasing implies (inferior_realsequence seq).n = seq.n
proof
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  assume
A1: seq is non-decreasing;
  (inferior_realsequence seq).n = lower_bound Y1 by Def4;
  hence thesis by A1,Th34;
end;

theorem
  seq is non-decreasing implies inferior_realsequence seq = seq
proof
  assume seq is non-decreasing;
  then for n being Element of NAT holds
   (inferior_realsequence seq).n = seq.n by Lm2;
  hence thesis by FUNCT_2:63;
end;

theorem Th65:
  seq is non-decreasing bounded_above implies seq.n <= (
  superior_realsequence seq).(n+1)
proof
  reconsider Y1 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
A1: seq.(n+1) in Y1;
  assume
A2: seq is non-decreasing bounded_above;
  then Y1 is bounded_above by Th31;
  then
A3: seq.(n+1) <= upper_bound Y1 by A1,SEQ_4:def 1;
A4: (superior_realsequence seq).(n+1) = upper_bound Y1 by Def5;
  seq.n <= seq.(n+1) by A2;
  hence thesis by A4,A3,XXREAL_0:2;
end;

theorem Th66:
  seq is non-decreasing bounded_above implies (
  superior_realsequence seq).n = (superior_realsequence seq).(n+1)
proof
  assume
A1: seq is non-decreasing bounded_above;
  then seq.n <= (superior_realsequence seq).(n+1) by Th65;
  then max((superior_realsequence seq).(n+1),seq.n) = (superior_realsequence
  seq).(n+1) by XXREAL_0:def 10;
  hence thesis by A1,Th47;
end;

theorem Th67:
  seq is non-decreasing bounded_above implies (
  superior_realsequence seq).n = upper_bound seq & (superior_realsequence seq)
   is
  constant
proof
  reconsider ubs = upper_bound seq as Element of REAL by XREAL_0:def 1;
  defpred P[Nat] means (superior_realsequence seq).$1 = ubs;
  assume
A1: seq is non-decreasing bounded_above;
A2: for k being Nat st P[k] holds P[k+1]
  by A1,Th66;
A3: P[0] by A1,Th39;
  for k being Nat holds P[k] from NAT_1:sch 2(A3,A2);
  hence thesis by VALUED_0:def 18;
end;

theorem
  seq is non-decreasing bounded_above implies
  lower_bound (superior_realsequence
  seq) = upper_bound seq
proof
  assume
A1: seq is non-decreasing bounded_above;
  then (superior_realsequence seq) is constant by Th67;
  then consider r1 being Element of REAL such that
A2: rng (superior_realsequence seq)={r1} by FUNCT_2:111;
  r1 in rng (superior_realsequence seq) by A2,TARSKI:def 1;
  then ex n being Element of NAT
st r1 = (superior_realsequence seq).n by FUNCT_2:113;
  then rng (superior_realsequence seq)= {upper_bound seq} by A1,A2,Th67;
  hence thesis by SEQ_4:9;
end;

theorem
  seq is non-increasing implies (superior_realsequence seq).(n+1) <= seq .n
proof
  reconsider Y1 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
A1: (superior_realsequence seq).(n+1) = upper_bound Y1 by Def5;
  assume
A2: seq is non-increasing;
  then upper_bound Y1 = seq.(n+1) by Th35;
  hence thesis by A2,A1;
end;

Lm3: seq is non-increasing implies (superior_realsequence seq).n = seq.n
proof
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  assume
A1: seq is non-increasing;
  (superior_realsequence seq).n = upper_bound Y1 by Def5;
  hence thesis by A1,Th35;
end;

theorem
  seq is non-increasing implies superior_realsequence seq = seq
proof
  assume seq is non-increasing;
  then for n being Element of NAT holds
   (superior_realsequence seq).n = seq.n by Lm3;
  hence thesis by FUNCT_2:63;
end;

theorem Th71:
  seq is non-increasing bounded_below implies (
  inferior_realsequence seq).(n+1) <= seq.n
proof
  reconsider Y1 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
A1: seq.(n+1) in Y1;
  assume
A2: seq is non-increasing bounded_below;
  then Y1 is bounded_below by Th32;
  then
A3: lower_bound Y1 <= seq.(n+1) by A1,SEQ_4:def 2;
A4: (inferior_realsequence seq).(n+1) = lower_bound Y1 by Def4;
  seq.(n+1) <= seq.n by A2;
  hence thesis by A4,A3,XXREAL_0:2;
end;

theorem Th72:
  seq is non-increasing bounded_below implies (
  inferior_realsequence seq).n = (inferior_realsequence seq).(n+1)
proof
  assume
A1: seq is non-increasing bounded_below;
  then (inferior_realsequence seq).(n+1) <= seq.n by Th71;
  then min((inferior_realsequence seq).(n+1),seq.n) = (inferior_realsequence
  seq).(n+1) by XXREAL_0:def 9;
  hence thesis by A1,Th46;
end;

theorem Th73:
  seq is non-increasing & seq is bounded_below implies (
  inferior_realsequence seq).n = lower_bound seq &
  (inferior_realsequence seq) is
  constant
proof
  assume that
A1: seq is non-increasing and
A2: seq is bounded_below;
   reconsider lbs = lower_bound seq as Element of REAL by XREAL_0:def 1;
  defpred P[Nat] means (inferior_realsequence seq).$1 = lbs;
A3: for k being Nat st P[k] holds P[k+1]
  by A1,A2,Th72;
A4: P[0] by A2,Th38;
  for k being Nat holds P[k] from NAT_1:sch 2(A4,A3);
  hence thesis by VALUED_0:def 18;
end;

theorem
  seq is non-increasing bounded_below implies upper_bound inferior_realsequence
  seq = lower_bound seq
proof
  assume
A1: seq is non-increasing bounded_below;
  then inferior_realsequence seq is constant by Th73;
  then consider r1 being Element of REAL such that
A2: rng inferior_realsequence seq={r1} by FUNCT_2:111;
  r1 in rng inferior_realsequence seq by A2,TARSKI:def 1;
  then ex n being Element of NAT
st r1 = (inferior_realsequence seq).n by FUNCT_2:113;
  then upper_bound inferior_realsequence seq =
  upper_bound {lower_bound seq} by A1,A2,Th73
    .= lower_bound seq by SEQ_4:9;
  hence thesis;
end;

theorem Th75:
  seq1 is bounded & seq2 is bounded & (for n holds seq1.n <= seq2.
  n) implies (for n holds (superior_realsequence seq1).n <= (
superior_realsequence seq2).n) & for n holds (inferior_realsequence seq1).n <=
  (inferior_realsequence seq2).n
proof
  assume that
A1: seq1 is bounded and
A2: seq2 is bounded and
A3: for n holds seq1.n <= seq2.n;
  now
    let n;
    reconsider Y2 = {seq2.k2 : n <= k2} as Subset of REAL by Th29;
    reconsider Y1 = {seq1.k1 : n <= k1} as Subset of REAL by Th29;
A4: Y1 <> {} & Y2 <> {} by SETLIM_1:1;
A5: (inferior_realsequence seq1).n = lower_bound Y1 &
(inferior_realsequence seq2)
    .n = lower_bound Y2 by Def4;
    Y1 is real-bounded by A1,Th33;
    then
A6: Y1 is bounded_below;
    now
      let r;
      assume r in Y2;
      then consider k such that
A7:   r = seq2.k and
A8:   n <= k;
      seq1.k in Y1 by A8;
      then
A9:   lower_bound Y1 <= seq1.k by A6,SEQ_4:def 2;
      seq1.k <= r by A3,A7;
      hence lower_bound Y1 <= r by A9,XXREAL_0:2;
    end;
    then
A10: for r be Real st r in Y2 holds lower_bound Y1 <= r;
    Y2 is real-bounded by A2,Th33;
    then
A11: Y2 is bounded_above;
A12: now
      let r be Real;
      assume r in Y1;
      then consider k such that
A13:  r = seq1.k and
A14:  n <= k;
      seq2.k in Y2 by A14;
      then
A15:  seq2.k <= upper_bound Y2 by A11,SEQ_4:def 1;
      r <= seq2.k by A3,A13;
      hence r <= upper_bound Y2 by A15,XXREAL_0:2;
    end;
    (superior_realsequence seq1).n = upper_bound Y1 &
    (superior_realsequence seq2)
    .n = upper_bound Y2 by Def5;
    hence (superior_realsequence seq1).n <= (superior_realsequence seq2).n & (
inferior_realsequence seq1).n <= (inferior_realsequence seq2).n
     by A5,A4,A12,A10,SEQ_4:113,144;
  end;
  hence thesis;
end;

theorem
  seq1 is bounded_below & seq2 is bounded_below implies (
  inferior_realsequence(seq1+seq2)).n >= (inferior_realsequence seq1).n + (
  inferior_realsequence seq2).n
proof
  assume seq1 is bounded_below & seq2 is bounded_below;
  then seq1 ^\n is bounded_below & seq2 ^\n is bounded_below by SEQM_3:28;
  then lower_bound(seq1 ^\n + seq2 ^\n) >=
  lower_bound(seq1 ^\n) + lower_bound(seq2 ^\n) by Th15;
  then
A1: lower_bound((seq1+seq2) ^\n) >=
lower_bound(seq1 ^\n) + lower_bound(seq2 ^\n) by SEQM_3:15;
  (inferior_realsequence seq1).n =
  lower_bound(seq1 ^\n) & (inferior_realsequence
  seq2 ).n = lower_bound(seq2 ^\n) by Th36;
  hence thesis by A1,Th36;
end;

theorem
  seq1 is bounded_above & seq2 is bounded_above implies (
  superior_realsequence(seq1+seq2)).n <= (superior_realsequence seq1).n + (
  superior_realsequence seq2).n
proof
  assume seq1 is bounded_above & seq2 is bounded_above;
  then seq1 ^\n is bounded_above & seq2 ^\n is bounded_above by SEQM_3:27;
  then upper_bound(seq1 ^\n + seq2 ^\n) <=
  upper_bound(seq1 ^\n) + upper_bound(seq2 ^\n) by Th16;
  then
A1: upper_bound((seq1+seq2) ^\n) <=
upper_bound(seq1 ^\n) + upper_bound(seq2 ^\n) by SEQM_3:15;
  (superior_realsequence seq1).n = upper_bound(seq1 ^\n) &
  (superior_realsequence
  seq2 ).n = upper_bound(seq2 ^\n) by Th37;
  hence thesis by A1,Th37;
end;

theorem
  seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative
implies (inferior_realsequence(seq1(#)seq2)).n >= (inferior_realsequence seq1).
  n * (inferior_realsequence seq2).n
proof
  assume seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative;
  then seq1 ^\n is bounded_below nonnegative & seq2 ^\n is bounded_below
  nonnegative by Th17,SEQM_3:28;
  then lower_bound((seq1 ^\n)(#)(seq2 ^\n))>=
  lower_bound(seq1 ^\n) * lower_bound(seq2 ^\n) by Th20;
  then
A1: lower_bound((seq1 (#) seq2) ^\n) >=
lower_bound(seq1 ^\n) * lower_bound(seq2 ^\n) by SEQM_3:19;
  (inferior_realsequence seq1).n = lower_bound(seq1 ^\n) &
  (inferior_realsequence
  seq2 ).n = lower_bound(seq2 ^\n) by Th36;
  hence thesis by A1,Th36;
end;

theorem Th79:
  seq1 is bounded_below nonnegative & seq2 is bounded_below
  nonnegative implies (inferior_realsequence(seq1(#)seq2)).n >= (
  inferior_realsequence seq1).n * (inferior_realsequence seq2).n
proof
  assume seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative;
  then seq1 ^\n is bounded_below nonnegative & seq2 ^\n is bounded_below
  nonnegative by Th17,SEQM_3:28;
  then lower_bound((seq1 ^\n)(#)(seq2 ^\n))>=
  lower_bound(seq1 ^\n) * lower_bound(seq2 ^\n) by Th20;
  then
A1: lower_bound((seq1 (#) seq2) ^\n) >=
lower_bound(seq1 ^\n) * lower_bound(seq2 ^\n) by SEQM_3:19;
  (inferior_realsequence seq1).n = lower_bound(seq1 ^\n) &
  (inferior_realsequence
  seq2 ).n = lower_bound(seq2 ^\n) by Th36;
  hence thesis by A1,Th36;
end;

theorem Th80:
  seq1 is bounded_above nonnegative & seq2 is bounded_above
  nonnegative implies (superior_realsequence(seq1(#)seq2)).n <= (
  superior_realsequence seq1).n * (superior_realsequence seq2).n
proof
  assume seq1 is bounded_above nonnegative & seq2 is bounded_above nonnegative;
  then seq1 ^\n is bounded_above nonnegative & seq2 ^\n is bounded_above
  nonnegative by Th17,SEQM_3:27;
  then upper_bound((seq1 ^\n)(#)(seq2 ^\n))<=
  upper_bound(seq1 ^\n) * upper_bound(seq2 ^\n) by Th21;
  then
A1: upper_bound((seq1 (#) seq2) ^\n) <=
upper_bound(seq1 ^\n) * upper_bound(seq2 ^\n) by SEQM_3:19;
  (superior_realsequence seq1).n = upper_bound(seq1 ^\n) &
  (superior_realsequence
  seq2 ).n = upper_bound(seq2 ^\n) by Th37;
  hence thesis by A1,Th37;
end;

definition
  let seq be Real_Sequence;
  func lim_sup seq -> Real equals
  lower_bound superior_realsequence seq;
  coherence;
end;

definition
  let seq be Real_Sequence;
  func lim_inf seq -> Real equals
  upper_bound inferior_realsequence seq;
  coherence;
end;

theorem Th81:
  seq is bounded implies (lim_inf seq <= r iff for s st 0<s holds
  for n ex k st seq.(n+k)<r+s )
proof
  set seq1 = inferior_realsequence seq;
  assume
A1: seq is bounded;
  then
A2: seq1 is bounded by Th56;
  thus lim_inf seq <= r implies for s st 0<s holds for n ex k st seq.(n+k)<r+s
  proof
    assume
A3: lim_inf seq <= r;
    let s such that
A4: 0<s;
    for n ex k st seq.(n+k)<r+s
    proof
      let n;
      consider k such that
A5:   seq.(n+k) < seq1.n+s by A1,A4,Th40;
      seq1.n <= r by A2,A3,Th9;
      then seq.(n+k)+seq1.n < r+(seq1.n+s) by A5,XREAL_1:8;
      then seq.(n+k) < r+(seq1.n+s)-seq1.n by XREAL_1:20;
      hence thesis;
    end;
    hence thesis;
  end;
  assume
A6: for s st 0<s holds for n ex k st seq.(n+k)<r+s;
  for s st 0<s holds lim_inf seq<=r+s
  proof
    let s such that
A7: 0<s;
    for n holds seq1.n <= r+s
    proof
      let n;
      consider k such that
A8:   seq.(n+k)<r+s by A6,A7;
      seq1.n <= seq.(n+k) by A1,Th40;
      hence thesis by A8,XXREAL_0:2;
    end;
    hence thesis by Th9;
  end;
  hence thesis by XREAL_1:41;
end;

theorem Th82:
  seq is bounded implies (r <= lim_inf seq iff for s st 0<s holds
  ex n st for k holds r-s<seq.(n+k) )
proof
  set seq1 = inferior_realsequence seq;
  assume
A1: seq is bounded;
  then
A2: seq1 is bounded by Th56;
  thus r <= lim_inf seq implies for s st 0<s holds ex n st for k holds r-s<seq
  .(n+k)
  proof
    assume
A3: r <= lim_inf seq;
    let s such that
A4: 0<s;
    ex n st for k holds r-s<seq.(n+k)
    proof
      consider n1 be Nat such that
A5:   seq1.n1 > upper_bound seq1-s by A2,A4,Th7;
      seq1.n1 + upper_bound seq1 > r + (upper_bound seq1-s)
      by A3,A5,XREAL_1:8;
      then seq1.n1 + upper_bound seq1 > r - s + upper_bound seq1;
      then
A6:   (seq1.n1 + upper_bound seq1) - upper_bound seq1 > r-s by XREAL_1:20;
      now
        let k;
        seq1.n1 <= seq.(n1+k) by A1,Th40;
        then (r-s) + seq1.n1 < seq.(n1+k) + seq1.n1 by A6,XREAL_1:8;
        then (r-s) + seq1.n1 - seq1.n1 < seq.(n1+k) by XREAL_1:19;
        hence r-s<seq.(n1+k);
      end;
      hence thesis;
    end;
    hence thesis;
  end;
  assume
A7: for s st 0<s holds ex n st for k holds r-s<seq.(n+k);
  for s st 0<s holds r-s<=lim_inf seq
  proof
    let s;
    assume 0<s;
    then consider n1 be Nat such that
A8: for k holds r-s<seq.(n1+k) by A7;
    for k holds r-s<=seq.(n1+k) by A8;
    then
A9: r-s <= seq1.n1 by A1,Th42;
    seq1.n1 <= upper_bound seq1 by A2,Th7;
    hence thesis by A9,XXREAL_0:2;
  end;
  hence thesis by XREAL_1:57;
end;

theorem
  seq is bounded implies (r = lim_inf seq iff for s st 0<s holds (for n
  ex k st seq.(n+k)<r+s) & ex n st for k holds r-s<seq.(n+k) )
proof
  assume
A1: seq is bounded;
  hence
  r = lim_inf seq implies for s st 0<s holds (for n ex k st seq.(n+k)<r+s
  ) & ex n st for k holds r-s<seq.(n+k) by Th81,Th82;
  assume
A2: for s st 0<s holds (for n ex k st seq.(n+k)<r+s) & ex n st for k
  holds r-s<seq.(n+k);
  then for s st 0<s holds ex n st for k holds r-s<seq.(n+k);
  then
A3: r <= lim_inf seq by A1,Th82;
  for s st 0<s holds for n ex k st seq.(n+k)<r+s by A2;
  then lim_inf seq <= r by A1,Th81;
  hence thesis by A3,XXREAL_0:1;
end;

theorem Th84:
  seq is bounded implies (r <= lim_sup seq iff for s st 0<s holds
  for n ex k st seq.(n+k)>r-s )
proof
  set seq1 = superior_realsequence seq;
  assume
A1: seq is bounded;
  then
A2: seq1 is bounded by Th56;
  thus r <= lim_sup seq implies for s st 0<s holds for n ex k st seq.(n+k)>r-s
  proof
    assume
A3: r <= lim_sup seq;
    let s such that
A4: 0<s;
    for n ex k st seq.(n+k)>r-s
    proof
      let n;
      consider k such that
A5:   seq.(n+k) > seq1.n-s by A1,A4,Th41;
      seq1.n >= r by A2,A3,Th10;
      then seq1.n+seq.(n+k) > r+(seq1.n-s) by A5,XREAL_1:8;
      then seq.(n+k) > r+seq1.n-s-seq1.n by XREAL_1:19;
      hence thesis;
    end;
    hence thesis;
  end;
  assume
A6: for s st 0<s holds for n ex k st seq.(n+k)>r-s;
  for s st 0<s holds lim_sup seq>=r-s
  proof
    let s such that
A7: 0<s;
    for n holds r-s <= seq1.n
    proof
      let n;
      consider k such that
A8:   r-s<seq.(n+k) by A6,A7;
      seq.(n+k) <= seq1.n by A1,Th41;
      hence thesis by A8,XXREAL_0:2;
    end;
    hence thesis by Th10;
  end;
  hence thesis by XREAL_1:57;
end;

theorem Th85:
  seq is bounded implies (lim_sup seq <= r iff for s st 0<s holds
  ex n st for k holds seq.(n+k)<r+s )
proof
  set seq1 = superior_realsequence seq;
  assume
A1: seq is bounded;
  then
A2: seq1 is bounded by Th56;
  thus lim_sup seq <= r implies for s st 0<s holds ex n st for k holds seq.(n+
  k)<r+s
  proof
    assume
A3: lim_sup seq <= r;
    for s st 0<s holds ex n st for k holds seq.(n+k)<r+s
    proof
      let s such that
A4:   0<s;
      ex n st for k holds seq.(n+k)<r+s
      proof
        consider n1 be Nat such that
A5:     seq1.n1 < lower_bound seq1+s by A2,A4,Th8;
        seq1.n1 + lower_bound seq1 < r + (lower_bound seq1+s)
        by A3,A5,XREAL_1:8;
        then seq1.n1 + lower_bound seq1 < r + s + lower_bound seq1;
        then
A6:     (seq1.n1 + lower_bound seq1) - lower_bound seq1 < r+s by XREAL_1:19;
        now
          let k;
          seq.(n1+k) <= seq1.n1 by A1,Th41;
          then seq.(n1+k) + seq1.n1 < (r+s) + seq1.n1 by A6,XREAL_1:8;
          then seq.(n1+k) + seq1.n1 - seq1.n1 < (r+s) by XREAL_1:19;
          hence seq.(n1+k) < r+s;
        end;
        hence thesis;
      end;
      hence thesis;
    end;
    hence thesis;
  end;
  assume
A7: for s st 0<s holds ex n st for k holds seq.(n+k)<r+s;
  for s st 0<s holds lim_sup seq<=r+s
  proof
    let s;
    assume 0<s;
    then consider n1 be Nat such that
A8: for k holds seq.(n1+k)<r+s by A7;
    for k holds seq.(n1+k)<=r+s by A8;
    then
A9: seq1.n1<=r+s by A1,Th44;
    lower_bound seq1 <= seq1.n1 by A2,Th8;
    hence thesis by A9,XXREAL_0:2;
  end;
  hence thesis by XREAL_1:41;
end;

theorem
  seq is bounded implies (r = lim_sup seq iff for s st 0<s holds (for n
  holds ex k st seq.(n+k)>r-s) & ex n st for k holds seq.(n+k)<r+s )
proof
  assume
A1: seq is bounded;
  hence
  r = lim_sup seq implies for s st 0<s holds (for n holds ex k st seq.(n+
  k)>r-s) & ex n st for k holds seq.(n+k)<r+s by Th84,Th85;
  assume
A2: for s st 0<s holds (for n holds ex k st seq.(n+k)>r-s) & ex n st for
  k holds seq.(n+k)<r+s;
  then for s st 0<s holds ex n st for k holds seq.(n+k)<r+s;
  then
A3: lim_sup seq <= r by A1,Th85;
  for s st 0<s holds for n holds ex k st seq.(n+k)>r-s by A2;
  then r <= lim_sup seq by A1,Th84;
  hence thesis by A3,XXREAL_0:1;
end;

theorem
  seq is bounded implies lim_inf seq <= lim_sup seq by Th55;

theorem Th88:
  seq is bounded & lim_sup seq = lim_inf seq iff seq is convergent
proof
  thus seq is bounded & lim_sup seq = lim_inf seq implies seq is convergent
  proof
    reconsider r= lower_bound superior_realsequence seq as Real;
    assume that
A1: seq is bounded and
A2: lim_sup seq = lim_inf seq;
A3: inferior_realsequence seq is bounded by A1,Th56;
A4: inferior_realsequence seq is non-decreasing by A1,Th50;
A5: superior_realsequence seq is non-increasing by A1,Th51;
A6: superior_realsequence seq is bounded by A1,Th56;
    for s st 0<s ex n st for m st n<=m holds |.seq.m-r.| < s
    proof
      let s such that
A7:   0 < s;
      consider k2 be Nat such that
A8:   (superior_realsequence seq).k2 < r + s by A6,A7,Th8;
      consider k1 be Nat such that
A9:   r - s < (inferior_realsequence seq).k1 by A2,A3,A7,Th7;
      reconsider k = max(k1,k2) as Nat by TARSKI:1;
      k2 <= k by XXREAL_0:25;
      then
A10:  (superior_realsequence seq).k <= (superior_realsequence seq).k2
      by A5,SEQM_3:8;
      k1 <= k by XXREAL_0:25;
      then
A11:  (inferior_realsequence seq).k1 <= (inferior_realsequence seq). k
      by A4,SEQM_3:6;
      ex n st for m st n<=m holds |.seq.m-r.| < s
      proof
        take k;
        let m;
        assume k <= m;
        then consider k3 being Nat such that
A12:    m = k + k3 by NAT_1:10;
        seq.m <= (superior_realsequence seq).k by A1,A12,Th41;
        then seq.m <= (superior_realsequence seq).k2 by A10,XXREAL_0:2;
        then
A13:    seq.m < r + s by A8,XXREAL_0:2;
        (inferior_realsequence seq).k <= seq.m by A1,A12,Th40;
        then (inferior_realsequence seq).k1 <= seq.m by A11,XXREAL_0:2;
        then r - s < seq.m by A9,XXREAL_0:2;
        hence thesis by A13,Th1;
      end;
      hence thesis;
    end;
    hence thesis by SEQ_2:def 6;
  end;
  assume
A14: seq is convergent;
  then consider r such that
A15: for p st 0 < p ex n st for m st n<=m holds |.seq.m-r.| < p by SEQ_2:def 6;
A16: seq is bounded by A14;
A17: for p st 0 < p ex n st r - p <= (inferior_realsequence seq).n & (
  superior_realsequence seq).n <= r + p
  proof
    let p;
    assume 0 < p;
    then consider n such that
A18: for m st n<=m holds |.seq.m-r.| < p by A15;
A19: for m st n<=m holds r - p <= seq.m & seq.m <= r + p
    proof
      let m;
      assume n<=m;
      then |.seq.m-r.| < p by A18;
      hence thesis by Th1;
    end;
    then for m st n<=m holds seq.m <= r + p;
    then
A20: (superior_realsequence seq).n <= r + p by A16,Th45;
    for m st n<=m holds r - p <= seq.m by A19;
    then r - p <= (inferior_realsequence seq).n by A16,Th43;
    hence thesis by A20;
  end;
A21: superior_realsequence seq is bounded & inferior_realsequence seq is
  bounded by A16,Th56;
A22: for p holds 0 < p implies r - p <= upper_bound inferior_realsequence seq &
 lower_bound
  superior_realsequence seq <= r + p
  proof
    let p;
    assume 0 < p;
    then consider n such that
A23: r - p <= (inferior_realsequence seq).n & (superior_realsequence
    seq).n <= r + p by A17;
    (inferior_realsequence seq).n <= upper_bound inferior_realsequence seq &
    lower_bound
    superior_realsequence seq <= (superior_realsequence seq).n by A21,Th7,Th8;
    hence thesis by A23,XXREAL_0:2;
  end;
  reconsider r as Real;
A24: for p holds 0 < p implies lower_bound superior_realsequence seq <= r + p
by A22;
  then
A25: lower_bound superior_realsequence seq <= r by XREAL_1:41;
  for p holds 0 < p implies r <= upper_bound inferior_realsequence seq + p
  proof
    let p;
    assume 0 < p;
    then r - p <= upper_bound inferior_realsequence seq by A22;
    hence thesis by XREAL_1:20;
  end;
  then
A26: r <= upper_bound inferior_realsequence seq by XREAL_1:41;
A27: upper_bound (inferior_realsequence seq) <=
lower_bound (superior_realsequence seq) by A14,Th55;
  lower_bound superior_realsequence seq <= r by A24,XREAL_1:41;
  then upper_bound inferior_realsequence seq <= r by A27,XXREAL_0:2;
  then r = upper_bound inferior_realsequence seq by A26,XXREAL_0:1;
  hence thesis by A14,A27,A25,XXREAL_0:1;
end;

theorem
  seq is convergent implies lim seq = lim_sup seq & lim seq = lim_inf seq
proof
  reconsider r= lim seq as Real;
  assume
A1: seq is convergent;
  then
A2: upper_bound(inferior_realsequence seq) <=
lower_bound(superior_realsequence seq) by Th55;
A3: seq is bounded by A1;
  then
A4: superior_realsequence seq is bounded & inferior_realsequence seq is
  bounded by Th56;
A5: for p holds 0 < p implies r - p <= upper_bound inferior_realsequence seq &
 lower_bound
  superior_realsequence seq <= r + p
  proof
    let p;
    assume 0 < p;
    then consider k such that
A6: for m st k <= m holds |.seq.m-r.|<p by A1,SEQ_2:def 7;
A7: for m st k <= m holds r - p <= seq.m & seq.m <= r + p
    proof
      let m;
      assume k <= m;
      then |.seq.m - r.| < p by A6;
      hence thesis by Th1;
    end;
    then for m st k <= m holds r - p <= seq.m;
    then
A8: r - p <= (inferior_realsequence seq).k by A3,Th43;
    for m st k <= m holds seq.m <= r + p by A7;
    then
A9: (superior_realsequence seq).k <= r + p by A3,Th45;
    (inferior_realsequence seq).k <= upper_bound inferior_realsequence seq &
     lower_bound
    superior_realsequence seq <= (superior_realsequence seq).k by A4,Th7,Th8;
    hence thesis by A8,A9,XXREAL_0:2;
  end;
A10: for p holds 0 < p implies r <= upper_bound inferior_realsequence seq + p
  proof
    let p;
    assume 0 < p;
    then r - p <= upper_bound inferior_realsequence seq by A5;
    hence thesis by XREAL_1:20;
  end;
  then
A11: r <= upper_bound inferior_realsequence seq by XREAL_1:41;
  r <= upper_bound inferior_realsequence seq by A10,XREAL_1:41;
  then
A12: r <= lower_bound superior_realsequence seq by A2,XXREAL_0:2;
  for p holds 0 < p implies lower_bound superior_realsequence seq <=
   r + p by A5;
  then
A13: lower_bound superior_realsequence seq <= r by XREAL_1:41;
  then upper_bound inferior_realsequence seq <= r by A2,XXREAL_0:2;
  hence thesis by A13,A11,A12,XXREAL_0:1;
end;

theorem Th90:
  seq is bounded implies lim_sup -seq = - lim_inf seq & lim_inf -
  seq = - lim_sup seq
proof
  assume
A1: seq is bounded;
  then inferior_realsequence seq is bounded by Th56;
  then
A2: - lim_inf seq = - - lower_bound - inferior_realsequence seq by Th13
    .= lower_bound - -superior_realsequence(-seq) by A1,Th61
    .= lim_sup -seq;
  superior_realsequence seq is bounded by A1,Th56;
  then - lim_sup seq = - - upper_bound - superior_realsequence seq by Th14
    .= upper_bound - -inferior_realsequence(-seq) by A1,Th62
    .= lim_inf -seq;
  hence thesis by A2;
end;

theorem
  seq1 is bounded & seq2 is bounded & (for n holds seq1.n <= seq2.n)
  implies lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2
proof
  assume that
A1: seq1 is bounded and
A2: seq2 is bounded and
A3: for n holds seq1.n <= seq2.n;
A4: superior_realsequence seq1 is convergent & inferior_realsequence seq1 is
  convergent by A1,Th57,Th58;
  superior_realsequence seq2 is bounded by A2,Th56;
  then
A5: lim superior_realsequence seq2 = lower_bound superior_realsequence seq2
by A2,Th25,Th51;
  inferior_realsequence seq1 is bounded by A1,Th56;
  then
A6: lim inferior_realsequence seq1 = upper_bound inferior_realsequence seq1
by A1,Th24,Th50;
  superior_realsequence seq1 is bounded by A1,Th56;
  then
A7: lim superior_realsequence seq1 = lower_bound superior_realsequence seq1
by A1,Th25,Th51;
A8: superior_realsequence seq2 is convergent & inferior_realsequence seq2 is
  convergent by A2,Th57,Th58;
  inferior_realsequence seq2 is bounded by A2,Th56;
  then
A9: lim inferior_realsequence seq2 = upper_bound inferior_realsequence seq2
by A2,Th24,Th50;
  ( for n holds (superior_realsequence seq1).n <= (superior_realsequence
seq2).n) & for n holds (inferior_realsequence seq1).n <= (inferior_realsequence
  seq2).n by A1,A2,A3,Th75;
  hence thesis by A4,A8,A7,A6,A5,A9,SEQ_2:18;
end;

theorem
  seq1 is bounded & seq2 is bounded implies lim_inf seq1 + lim_inf seq2
  <= lim_inf (seq1+seq2) & lim_inf (seq1+seq2) <= lim_inf seq1 + lim_sup seq2 &
  lim_inf (seq1+seq2) <= lim_sup seq1 + lim_inf seq2 & lim_inf seq1 + lim_sup
seq2 <= lim_sup (seq1+seq2) & lim_sup seq1 + lim_inf seq2 <= lim_sup (seq1+seq2
) & lim_sup (seq1+seq2) <= lim_sup seq1 + lim_sup seq2 & (seq1 is convergent or
seq2 is convergent implies lim_inf (seq1+seq2) = lim_inf seq1 + lim_inf seq2 &
  lim_sup (seq1+seq2) = lim_sup seq1 + lim_sup seq2 )
proof
  assume
A1: seq1 is bounded & seq2 is bounded;
A2: for seq1,seq2 st seq1 is bounded & seq2 is bounded holds lim_sup (seq1+
  seq2) <= lim_sup seq1 + lim_sup seq2
  proof
    let seq1,seq2;
    set r1 = lim_sup seq1, r2 = lim_sup seq2;
    assume that
A3: seq1 is bounded and
A4: seq2 is bounded;
    for s st 0<s holds ex n st for k holds (seq1+seq2).(n+k) < r1+r2+s
    proof
      let s;
      assume 0<s;
      then
A5:   0<s/2 by XREAL_1:215;
      then consider n1 being Nat such that
A6:   for k holds seq1.(n1+k) < r1+s/2 by A3,Th85;
      consider n2 being Nat such that
A7:   for k holds seq2.(n2+k) < r2+s/2 by A4,A5,Th85;
      for k holds (seq1+seq2).(n1+n2+k) < r1+r2+s
      proof
        let k;
        seq1.(n1+(n2+k)) < r1+s/2 & seq2.(n2+(n1+k)) < r2+s/2 by A6,A7;
        then seq1.(n1+n2+k) + seq2.(n1+n2+k) < (r1+s/2)+(r2+s/2) by XREAL_1:8;
        hence thesis by SEQ_1:7;
      end;
      hence thesis;
    end;
    hence thesis by A3,A4,Th85;
  end;
A8: for seq1,seq2 st seq1 is bounded & seq2 is bounded holds lim_inf seq1 +
  lim_sup seq2 <= lim_sup (seq1+seq2)
  proof
    let seq1,seq2;
    assume that
A9: seq1 is bounded and
A10: seq2 is bounded;
    lim_sup ((seq1+seq2)+(-seq1)) <= lim_sup (-seq1) + lim_sup (seq1+
    seq2) by A2,A9,A10;
    then lim_sup (seq1+seq2+-seq1) <= -lim_inf seq1 + lim_sup (seq1+seq2) by A9
,Th90;
    then lim_sup (seq2+seq1-seq1) <= lim_sup (seq1+seq2) - lim_inf seq1;
    then lim_sup seq2 <= lim_sup (seq1+seq2) - lim_inf seq1 by Th2;
    hence thesis by XREAL_1:19;
  end;
  then
A11: lim_inf seq1 + lim_sup seq2 <= lim_sup (seq1+seq2) by A1;
A12: lim_sup seq1 + lim_inf seq2 <= lim_sup (seq1+seq2) by A8,A1;
A13: lim_sup (seq1+seq2) <= lim_sup seq1 + lim_sup seq2 by A2,A1;
A14: for seq1,seq2 st seq1 is bounded & seq2 is bounded holds lim_inf seq1 +
  lim_inf seq2 <= lim_inf (seq1+seq2)
  proof
    let seq1,seq2;
    set r1 = lim_inf seq1, r2 = lim_inf seq2;
    assume that
A15: seq1 is bounded and
A16: seq2 is bounded;
    for s st 0<s holds ex n st for k holds r1+r2-s < (seq1+seq2).(n+k)
    proof
      let s;
      assume 0<s;
      then
A17:  0<s/2 by XREAL_1:215;
      then consider n1 being Nat such that
A18:  for k holds r1-s/2 < seq1.(n1+k) by A15,Th82;
      consider n2 being Nat such that
A19:  for k holds r2-s/2 < seq2.(n2+k) by A16,A17,Th82;
      for k holds r1+r2-s < (seq1+seq2).(n1+n2+k)
      proof
        let k;
        r1-s/2 < seq1.(n1+(n2+k)) & r2-s/2 < seq2.(n2+(n1+k)) by A18,A19;
        then (r1-s/2)+(r2-s/2) < seq1.(n1+n2+k) + seq2.(n1+n2+k) by XREAL_1:8;
        hence thesis by SEQ_1:7;
      end;
      hence thesis;
    end;
    hence thesis by A15,A16,Th82;
  end;
  then
A20: lim_inf seq1 + lim_inf seq2 <= lim_inf (seq1+seq2) by A1;
A21: for seq1,seq2 st seq1 is bounded & seq2 is bounded holds lim_inf (seq1+
  seq2) <= lim_inf seq1 + lim_sup seq2
  proof
    let seq1,seq2;
    assume that
A22: seq1 is bounded and
A23: seq2 is bounded;
    lim_inf ((seq1+seq2)+(-seq2)) >= lim_inf (seq1+seq2) + lim_inf (-
    seq2) by A14,A22,A23;
    then lim_inf (seq1+seq2+-seq2) >= lim_inf (seq1+seq2) +- lim_sup seq2 by
A23,Th90;
    then lim_inf (seq1+seq2-seq2) >= lim_inf (seq1+seq2) - lim_sup seq2;
    then lim_inf seq1 >= lim_inf (seq1+seq2) - lim_sup seq2 by Th2;
    hence thesis by XREAL_1:20;
  end;
  then
A24: lim_inf (seq1+seq2) <= lim_sup seq1 + lim_inf seq2 by A1;
A25: lim_inf (seq1+seq2) <= lim_inf seq1 + lim_sup seq2 by A21,A1;
  seq1 is convergent or seq2 is convergent implies lim_inf (seq1+seq2) =
lim_inf seq1 + lim_inf seq2 & lim_sup (seq1+seq2) = lim_sup seq1 + lim_sup seq2
  proof
    assume
A26: seq1 is convergent or seq2 is convergent;
    per cases by A26;
    suppose
      seq1 is convergent;
      then lim_inf seq1 = lim_sup seq1 by Th88;
      hence thesis by A20,A24,A11,A13,XXREAL_0:1;
    end;
    suppose
      seq2 is convergent;
      then lim_inf seq2 = lim_sup seq2 by Th88;
      hence thesis by A20,A25,A12,A13,XXREAL_0:1;
    end;
  end;
  hence thesis by A14,A21,A2,A8,A1;
end;

theorem
  seq1 is bounded nonnegative & seq2 is bounded nonnegative implies (
  lim_inf seq1) * (lim_inf seq2) <= lim_inf(seq1(#)seq2) & lim_sup(seq1(#)seq2)
  <= (lim_sup seq1) * (lim_sup seq2)
proof
A1: for seq1,seq2 st seq1 is bounded & seq1 is nonnegative & seq2 is
bounded & seq2 is nonnegative holds lim_sup(seq1(#)seq2) <= (lim_sup seq1) * (
  lim_sup seq2)
  proof
    let seq1,seq2;
    assume that
A2: seq1 is bounded nonnegative and
A3: seq2 is bounded nonnegative;
    set seq3 = superior_realsequence seq1, seq4 = superior_realsequence seq2,
    seq5 = superior_realsequence(seq1(#)seq2);
A4: seq5 is convergent by A2,A3,Th58;
A5: lower_bound seq5 = lim seq5 & lower_bound seq3 = lim seq3 by A2,A3,Th58;
A6: lower_bound seq4 =lim seq4 by A3,Th58;
A7: for n holds seq5.n <= (seq3(#)seq4).n
    proof
      let n;
      seq5.n <= seq3.n * seq4.n by A2,A3,Th80;
      hence thesis by SEQ_1:8;
    end;
A8: seq3 is convergent & seq4 is convergent by A2,A3,Th58;
    then (seq3(#)seq4) is convergent;
    then lim seq5 <= lim (seq3(#)seq4) by A4,A7,SEQ_2:18;
    hence thesis by A8,A5,A6,SEQ_2:15;
  end;
  for seq1,seq2 st seq1 is bounded nonnegative & seq2 is bounded
  nonnegative holds (lim_inf seq1) * (lim_inf seq2) <= lim_inf(seq1(#)seq2)
  proof
    let seq1,seq2;
    assume that
A9: seq1 is bounded nonnegative and
A10: seq2 is bounded nonnegative;
    set seq3 = inferior_realsequence seq1, seq4 = inferior_realsequence seq2,
    seq5 = inferior_realsequence(seq1(#)seq2);
A11: seq5 is convergent by A9,A10,Th57;
A12: upper_bound seq5 = lim seq5 & upper_bound seq3 = lim seq3 by A9,A10,Th57;
A13: upper_bound seq4 =lim seq4 by A10,Th57;
A14: for n holds seq5.n >= (seq3(#)seq4).n
    proof
      let n;
      seq5.n >= seq3.n * seq4.n by A9,A10,Th79;
      hence thesis by SEQ_1:8;
    end;
A15: seq3 is convergent & seq4 is convergent by A9,A10,Th57;
    then (seq3(#)seq4) is convergent;
    then lim seq5 >= lim (seq3(#)seq4) by A11,A14,SEQ_2:18;
    hence thesis by A15,A12,A13,SEQ_2:15;
  end;
  hence thesis by A1;
end;