rinfsup2.miz



    begin

    reserve n,m,k,k1,k2 for Nat;

    reserve X for non empty Subset of ExtREAL ;

    reserve Y for non empty Subset of REAL ;

    theorem :: RINFSUP2:1

    

     Th1: X = Y & Y is bounded_above implies X is bounded_above & ( sup X) = ( upper_bound Y)

    proof

      assume that

       A1: X = Y and

       A2: Y is bounded_above;

      

       A3: for s be Real st s in Y holds s <= ( sup X) by A1, XXREAL_2: 4;

       not -infty in X by A1;

      then

       A4: X <> { -infty } by TARSKI:def 1;

      for r be ExtReal st r in X holds r <= ( upper_bound Y) by A1, A2, SEQ_4:def 1;

      then

       A5: ( upper_bound Y) is UpperBound of X by XXREAL_2:def 1;

      hence X is bounded_above by XXREAL_2:def 10;

      then ( sup X) in REAL by A4, XXREAL_2: 57;

      then

       A6: ( upper_bound Y) <= ( sup X) by A3, SEQ_4: 45;

      ( sup X) <= ( upper_bound Y) by A5, XXREAL_2:def 3;

      hence thesis by A6, XXREAL_0: 1;

    end;

    theorem :: RINFSUP2:2

    X = Y & X is bounded_above implies Y is bounded_above & ( sup X) = ( upper_bound Y) by Th1;

    theorem :: RINFSUP2:3

    

     Th3: X = Y & Y is bounded_below implies X is bounded_below & ( inf X) = ( lower_bound Y)

    proof

      assume that

       A1: X = Y and

       A2: Y is bounded_below;

      

       A3: for s be Real st s in Y holds ( inf X) <= s by A1, XXREAL_2: 3;

       not +infty in X by A1;

      then

       A4: X <> { +infty } by TARSKI:def 1;

      for r be ExtReal st r in X holds ( lower_bound Y) <= r by A1, A2, SEQ_4:def 2;

      then

       A5: ( lower_bound Y) is LowerBound of X by XXREAL_2:def 2;

      hence X is bounded_below by XXREAL_2:def 9;

      then ( inf X) in REAL by A4, XXREAL_2: 58;

      then

       A6: ( inf X) <= ( lower_bound Y) by A3, SEQ_4: 43;

      ( lower_bound Y) <= ( inf X) by A5, XXREAL_2:def 4;

      hence thesis by A6, XXREAL_0: 1;

    end;

    theorem :: RINFSUP2:4

    X = Y & X is bounded_below implies Y is bounded_below & ( inf X) = ( lower_bound Y) by Th3;

    definition

      let seq be ExtREAL_sequence;

      :: RINFSUP2:def1

      func sup seq -> Element of ExtREAL equals ( sup ( rng seq));

      coherence ;

      :: RINFSUP2:def2

      func inf seq -> Element of ExtREAL equals ( inf ( rng seq));

      coherence ;

    end

    definition

      let seq be ExtREAL_sequence;

      :: RINFSUP2:def3

      attr seq is bounded_below means ( rng seq) is bounded_below;

      :: RINFSUP2:def4

      attr seq is bounded_above means ( rng seq) is bounded_above;

    end

    definition

      let seq be ExtREAL_sequence;

      :: RINFSUP2:def5

      attr seq is bounded means seq is bounded_above & seq is bounded_below;

    end

    reserve seq for ExtREAL_sequence;

    theorem :: RINFSUP2:5

    

     Th5: for seq, n holds { (seq . k) : n <= k } is non empty Subset of ExtREAL

    proof

      let seq, n;

      deffunc F( Nat) = (seq . $1);

      defpred P[ Nat] means n <= $1;

      set Y = { F(k) : P[k] };

      

       A1: (seq . n) in Y;

      Y c= ExtREAL

      proof

        let x be object;

        assume x in Y;

        then

        consider k such that

         A2: F(k) = x and P[k];

        thus thesis by A2;

      end;

      hence thesis by A1;

    end;

    definition

      let seq be ExtREAL_sequence;

      :: RINFSUP2:def6

      func inferior_realsequence seq -> ExtREAL_sequence means

      : Def6: for n holds ex Y be non empty Subset of ExtREAL st Y = { (seq . k) : n <= k } & (it . n) = ( inf Y);

      existence

      proof

        defpred P[ Nat, Element of ExtREAL ] means ex Y be non empty Subset of ExtREAL st Y = { (seq . k) : $1 <= k } & $2 = ( inf Y);

        

         A1: for n be Element of NAT holds ex y be Element of ExtREAL st P[n, y]

        proof

          let n be Element of NAT ;

          reconsider Y = { (seq . k) : n <= k } as non empty Subset of ExtREAL by Th5;

          reconsider y = ( inf Y) as Element of ExtREAL ;

          take y;

          thus thesis;

        end;

        consider f be sequence of ExtREAL such that

         A2: for n be 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 ExtREAL_sequence such that

         A3: for n holds ex Y be non empty Subset of ExtREAL st Y = { (seq . k) : n <= k } & (seq1 . n) = ( inf Y) and

         A4: for n holds ex Y be non empty Subset of ExtREAL st Y = { (seq . k) : n <= k } & (seq2 . n) = ( inf Y);

        

         A5: for y be object st y in NAT holds (seq1 . y) = (seq2 . y)

        proof

          let y be object;

          assume y in NAT ;

          then

          reconsider n = y as Element of NAT ;

          

           A6: ex Z be non empty Subset of ExtREAL st Z = { (seq . k) : n <= k } & (seq2 . n) = ( inf Z) by A4;

          ex Y be non empty Subset of ExtREAL st Y = { (seq . k) : n <= k } & (seq1 . n) = ( inf Y) by A3;

          hence thesis by A6;

        end;

        

         A7: NAT = ( dom seq2) by FUNCT_2:def 1;

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

        hence thesis by A5, A7, FUNCT_1: 2;

      end;

    end

    definition

      let seq be ExtREAL_sequence;

      :: RINFSUP2:def7

      func superior_realsequence seq -> ExtREAL_sequence means

      : Def7: for n holds ex Y be non empty Subset of ExtREAL st Y = { (seq . k) where k : n <= k } & (it . n) = ( sup Y);

      existence

      proof

        defpred P[ Nat, Element of ExtREAL ] means ex Y be non empty Subset of ExtREAL st Y = { (seq . k) : $1 <= k } & $2 = ( sup Y);

        

         A1: for n be Element of NAT holds ex y be Element of ExtREAL st P[n, y]

        proof

          let n be Element of NAT ;

          reconsider Y = { (seq . k) : n <= k } as non empty Subset of ExtREAL by Th5;

          reconsider y = ( sup Y) as Element of ExtREAL ;

          take y;

          thus thesis;

        end;

        consider f be sequence of ExtREAL such that

         A2: for n be 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 P[n, (f . n)] by A2;

      end;

      uniqueness

      proof

        let seq1,seq2 be ExtREAL_sequence such that

         A3: for n holds ex Y be non empty Subset of ExtREAL st Y = { (seq . k) : n <= k } & (seq1 . n) = ( sup Y) and

         A4: for m holds ex Y be non empty Subset of ExtREAL st Y = { (seq . k) : m <= k } & (seq2 . m) = ( sup Y);

        

         A5: for y be object st y in NAT holds (seq1 . y) = (seq2 . y)

        proof

          let y be object;

          assume y in NAT ;

          then

          reconsider n = y as Element of NAT ;

          

           A6: ex Z be non empty Subset of ExtREAL st Z = { (seq . k) : n <= k } & (seq2 . n) = ( sup Z) by A4;

          ex Y be non empty Subset of ExtREAL st Y = { (seq . k) : n <= k } & (seq1 . n) = ( sup Y) by A3;

          hence thesis by A6;

        end;

        

         A7: NAT = ( dom seq2) by FUNCT_2:def 1;

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

        hence thesis by A5, A7, FUNCT_1: 2;

      end;

    end

    theorem :: RINFSUP2:6

    seq is real-valued implies seq is Real_Sequence by FUNCT_2: 6;

    reserve e1,e2 for ExtReal;

    theorem :: RINFSUP2:7

    

     Th7: (seq is increasing iff for n,m be Nat st m < n holds (seq . m) < (seq . n)) & (seq is decreasing iff for n,m be Nat st m < n holds (seq . n) < (seq . m)) & (seq is non-decreasing iff for n,m be Nat st m <= n holds (seq . m) <= (seq . n)) & (seq is non-increasing iff for n,m be Nat st m <= n holds (seq . n) <= (seq . m))

    proof

      

       A1: ( dom seq) = NAT by FUNCT_2:def 1;

      thus seq is increasing implies for n,m be Nat st m < n holds (seq . m) < (seq . n)

      proof

        assume

         A2: seq is increasing;

        let n,m be Nat;

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

        hence thesis by A2, A1;

      end;

      thus (for n,m be Nat st m < n holds (seq . m) < (seq . n)) implies seq is increasing;

      thus seq is decreasing implies for n,m be Nat st m < n holds (seq . m) > (seq . n)

      proof

        assume

         A3: seq is decreasing;

        let n,m be Nat;

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

        hence thesis by A3, A1;

      end;

      thus (for n,m be Nat st m < n holds (seq . n) < (seq . m)) implies seq is decreasing;

      thus seq is non-decreasing implies for n,m be Nat st m <= n holds (seq . m) <= (seq . n)

      proof

        assume

         A4: seq is non-decreasing;

        let n,m be Nat;

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

        hence thesis by A4, A1;

      end;

      thus (for n,m be Nat st m <= n holds (seq . m) <= (seq . n)) implies seq is non-decreasing;

      thus seq is non-increasing implies for n,m be Nat st m <= n holds (seq . m) >= (seq . n)

      proof

        assume

         A5: seq is non-increasing;

        let n,m be Nat;

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

        hence thesis by A5, A1;

      end;

      assume

       A6: for n,m be Nat st m <= n holds (seq . n) <= (seq . m);

      let e1, e2;

      thus thesis by A6;

    end;

    theorem :: RINFSUP2:8

    

     Th8: (( inferior_realsequence seq) . n) <= (seq . n) & (seq . n) <= (( superior_realsequence seq) . n)

    proof

      consider Y be non empty Subset of ExtREAL such that

       A1: Y = { (seq . k) : n <= k } and

       A2: (( inferior_realsequence seq) . n) = ( inf Y) by Def6;

      

       A3: (seq . n) in Y by A1;

      hence (( inferior_realsequence seq) . n) <= (seq . n) by A2, XXREAL_2: 3;

      ex Z be non empty Subset of ExtREAL st Z = { (seq . k) : n <= k } & (( superior_realsequence seq) . n) = ( sup Z) by Def7;

      hence thesis by A1, A3, XXREAL_2: 4;

    end;

    

     Lm1: ( superior_realsequence seq) is non-increasing

    proof

      now

        let n,m be Nat;

        consider Y be non empty Subset of ExtREAL such that

         A1: Y = { (seq . k) : m <= k } and

         A2: (( superior_realsequence seq) . m) = ( sup Y) by Def7;

        consider Z be non empty Subset of ExtREAL such that

         A3: Z = { (seq . k) : n <= k } and

         A4: (( superior_realsequence seq) . n) = ( sup Z) by Def7;

        assume

         A5: m <= n;

        Z c= Y

        proof

          let z be object;

          assume z in Z;

          then

          consider k such that

           A6: z = (seq . k) and

           A7: n <= k by A3;

          m <= k by A5, A7, XXREAL_0: 2;

          hence thesis by A1, A6;

        end;

        hence (( superior_realsequence seq) . n) <= (( superior_realsequence seq) . m) by A2, A4, XXREAL_2: 59;

      end;

      hence thesis;

    end;

    

     Lm2: ( inferior_realsequence seq) is non-decreasing

    proof

      now

        let n,m be Nat;

        consider Y be non empty Subset of ExtREAL such that

         A1: Y = { (seq . k) : m <= k } and

         A2: (( inferior_realsequence seq) . m) = ( inf Y) by Def6;

        consider Z be non empty Subset of ExtREAL such that

         A3: Z = { (seq . k) : n <= k } and

         A4: (( inferior_realsequence seq) . n) = ( inf Z) by Def6;

        assume

         A5: m <= n;

        Z c= Y

        proof

          let z be object;

          assume z in Z;

          then

          consider k such that

           A6: z = (seq . k) and

           A7: n <= k by A3;

          m <= k by A5, A7, XXREAL_0: 2;

          hence thesis by A1, A6;

        end;

        hence (( inferior_realsequence seq) . m) <= (( inferior_realsequence seq) . n) by A2, A4, XXREAL_2: 60;

      end;

      hence thesis;

    end;

    registration

      let seq;

      cluster ( superior_realsequence seq) -> non-increasing;

      coherence by Lm1;

      cluster ( inferior_realsequence seq) -> non-decreasing;

      coherence by Lm2;

    end

    definition

      let seq be ExtREAL_sequence;

      :: RINFSUP2:def8

      func lim_sup seq -> Element of ExtREAL equals ( inf ( superior_realsequence seq));

      coherence ;

      :: RINFSUP2:def9

      func lim_inf seq -> Element of ExtREAL equals ( sup ( inferior_realsequence seq));

      coherence ;

    end

    reserve rseq for Real_Sequence;

    theorem :: RINFSUP2:9

    

     Th9: seq = rseq & rseq is bounded implies ( superior_realsequence seq) = ( superior_realsequence rseq) & ( lim_sup seq) = ( lim_sup rseq)

    proof

      assume that

       A1: seq = rseq and

       A2: rseq is bounded;

      

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

       A4:

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider n = x as Element of NAT ;

        now

          let x be object;

          assume x in { (rseq . k) : n <= k };

          then ex k st x = (rseq . k) & n <= k;

          hence x in REAL by XREAL_0:def 1;

        end;

        then

        reconsider Y2 = { (rseq . k) : n <= k } as Subset of REAL by TARSKI:def 3;

        

         A5: Y2 is bounded_above by A2, RINFSUP1: 31;

        ex Y1 be non empty Subset of ExtREAL st Y1 = { (seq . k) : n <= k } & (( superior_realsequence seq) . n) = ( sup Y1) by Def7;

        then (( superior_realsequence seq) . x) = ( upper_bound Y2) by A1, A5, Th1;

        hence (( superior_realsequence seq) . x) = (( superior_realsequence rseq) . x) by RINFSUP1:def 5;

      end;

      ( superior_realsequence rseq) is bounded by A2, RINFSUP1: 56;

      then

       A6: ( rng ( superior_realsequence rseq)) is bounded_below by RINFSUP1: 6;

       NAT = ( dom ( superior_realsequence seq)) by FUNCT_2:def 1;

      then ( superior_realsequence seq) = ( superior_realsequence rseq) by A4, A3, FUNCT_1: 2;

      hence thesis by A6, Th3;

    end;

    theorem :: RINFSUP2:10

    

     Th10: seq = rseq & rseq is bounded implies ( inferior_realsequence seq) = ( inferior_realsequence rseq) & ( lim_inf seq) = ( lim_inf rseq)

    proof

      assume that

       A1: seq = rseq and

       A2: rseq is bounded;

      

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

       A4:

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider n = x as Element of NAT ;

        consider Y1 be non empty Subset of ExtREAL such that

         A5: Y1 = { (seq . k) : n <= k } and

         A6: (( inferior_realsequence seq) . n) = ( inf Y1) by Def6;

        now

          let x be object;

          assume x in { (rseq . k) : n <= k };

          then ex k st x = (rseq . k) & n <= k;

          hence x in REAL by XREAL_0:def 1;

        end;

        then

        reconsider Y2 = { (rseq . k) : n <= k } as Subset of REAL by TARSKI:def 3;

        Y2 is bounded_below by A2, RINFSUP1: 32;

        then ( inf Y1) = ( lower_bound Y2) by A1, A5, Th3;

        hence (( inferior_realsequence seq) . x) = (( inferior_realsequence rseq) . x) by A6, RINFSUP1:def 4;

      end;

      ( inferior_realsequence rseq) is bounded by A2, RINFSUP1: 56;

      then

       A7: ( rng ( inferior_realsequence rseq)) is bounded_above by RINFSUP1: 5;

       NAT = ( dom ( inferior_realsequence seq)) by FUNCT_2:def 1;

      then ( inferior_realsequence seq) = ( inferior_realsequence rseq) by A4, A3, FUNCT_1: 2;

      hence thesis by A7, Th1;

    end;

    theorem :: RINFSUP2:11

    

     Th11: seq is bounded implies seq is Real_Sequence

    proof

      assume

       A1: seq is bounded;

      then seq is bounded_below;

      then ( rng seq) is bounded_below;

      then

      consider UL be Real such that

       A2: UL is LowerBound of ( rng seq) by XXREAL_2:def 9;

      

       A3: UL in REAL by XREAL_0:def 1;

      seq is bounded_above by A1;

      then ( rng seq) is bounded_above;

      then

      consider UB be Real such that

       A4: UB is UpperBound of ( rng seq) by XXREAL_2:def 10;

      

       A5: UB in REAL by XREAL_0:def 1;

       A6:

      now

        let x be object;

        assume x in NAT ;

        then

         A7: (seq . x) in ( rng seq) by FUNCT_2: 4;

        then

         A8: (seq . x) <> -infty by A2, A3, XXREAL_0: 12, XXREAL_2:def 2;

        (seq . x) <> +infty by A5, A4, A7, XXREAL_0: 9, XXREAL_2:def 1;

        hence (seq . x) in REAL by A8, XXREAL_0: 14;

      end;

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

      hence thesis by A6, FUNCT_2: 3;

    end;

    theorem :: RINFSUP2:12

    

     Th12: seq = rseq implies (seq is bounded_above iff rseq is bounded_above)

    proof

      assume

       A1: seq = rseq;

      hereby

        assume seq is bounded_above;

        then ( rng rseq) is bounded_above by A1;

        then

        consider p be Real such that

         A2: p is UpperBound of ( rng rseq) by XXREAL_2:def 10;

        

         A3: for y be Real st y in ( rng rseq) holds y <= p by A2, XXREAL_2:def 1;

        now

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          then (rseq . n) in ( rng rseq) by FUNCT_2: 4;

          then ( 0 + (rseq . n)) < (1 + p) by A3, XREAL_1: 8;

          hence (rseq . n) < (p + 1);

        end;

        hence rseq is bounded_above by SEQ_2:def 3;

      end;

      assume rseq is bounded_above;

      then

      consider q be Real such that

       A4: for n be Nat holds (rseq . n) < q by SEQ_2:def 3;

      now

        let r be ExtReal;

        assume r in ( rng seq);

        then ex x be object st x in ( dom rseq) & r = (rseq . x) by A1, FUNCT_1:def 3;

        hence r <= q by A4;

      end;

      then q is UpperBound of ( rng seq) by XXREAL_2:def 1;

      hence ( rng seq) is bounded_above by XXREAL_2:def 10;

    end;

    theorem :: RINFSUP2:13

    

     Th13: seq = rseq implies (seq is bounded_below iff rseq is bounded_below)

    proof

      assume

       A1: seq = rseq;

      hereby

        assume seq is bounded_below;

        then ( rng rseq) is bounded_below by A1;

        then

        consider p be Real such that

         A2: p is LowerBound of ( rng rseq) by XXREAL_2:def 9;

        

         A3: for y be Real st y in ( rng rseq) holds p <= y by A2, XXREAL_2:def 2;

        now

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          then (rseq . n) in ( rng rseq) by FUNCT_2: 4;

          then (p - 1) < ((rseq . n) - 0 ) by A3, XREAL_1: 15;

          hence (p - 1) < (rseq . n);

        end;

        hence rseq is bounded_below by SEQ_2:def 4;

      end;

      assume rseq is bounded_below;

      then

      consider q be Real such that

       A4: for n be Nat holds q < (rseq . n) by SEQ_2:def 4;

      now

        let r be ExtReal;

        assume r in ( rng seq);

        then ex x be object st x in ( dom rseq) & r = (rseq . x) by A1, FUNCT_1:def 3;

        hence q <= r by A4;

      end;

      then q is LowerBound of ( rng seq) by XXREAL_2:def 2;

      hence ( rng seq) is bounded_below by XXREAL_2:def 9;

    end;

    theorem :: RINFSUP2:14

    

     Th14: seq = rseq & rseq is convergent implies seq is convergent_to_finite_number & seq is convergent & ( lim seq) = ( lim rseq)

    proof

      assume that

       A1: seq = rseq and

       A2: rseq is convergent;

      reconsider lrs = ( lim rseq) as R_eal by XXREAL_0:def 1;

       A3:

      now

        let e be Real;

        assume 0 < e;

        then

        consider n be Nat such that

         A4: for m be Nat st n <= m holds |.((rseq . m) - ( lim rseq)) qua Complex.| < e by A2, SEQ_2:def 7;

        set N = n;

        now

          let m be Nat;

          

           A5: ((rseq . m) - ( lim rseq)) = ((seq . m) - ( lim rseq)) by A1, SUPINF_2: 3;

          assume N <= m;

          then |.((rseq . m) - ( lim rseq)) qua Complex.| < e by A4;

          hence |.((seq . m) - ( lim rseq)).| < e by A5, EXTREAL1: 12;

        end;

        hence ex N be Nat st for m be Nat st N <= m holds |.((seq . m) - lrs).| < e;

      end;

      then

       A6: seq is convergent_to_finite_number by MESFUNC5:def 8;

      then seq is convergent by MESFUNC5:def 11;

      hence thesis by A3, A6, MESFUNC5:def 12;

    end;

    theorem :: RINFSUP2:15

    

     Th15: seq = rseq & seq is convergent_to_finite_number implies rseq is convergent & ( lim seq) = ( lim rseq)

    proof

      assume that

       A1: seq = rseq and

       A2: seq is convergent_to_finite_number;

      

       A3: not (( lim seq) = +infty & seq is convergent_to_+infty) by A2, MESFUNC5: 50;

      

       A4: not (( lim seq) = -infty & seq is convergent_to_-infty) by A2, MESFUNC5: 51;

      seq is convergent by A2, MESFUNC5:def 11;

      then

      consider g be Real such that

       A5: ( lim seq) = g and

       A6: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - ( lim seq)).| < p and seq is convergent_to_finite_number by A3, A4, MESFUNC5:def 12;

      

       A7: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((rseq . m) - g) qua Complex.| < p

      proof

        let p be Real;

        assume 0 < p;

        then

        consider n be Nat such that

         A8: for m be Nat st n <= m holds |.((seq . m) - ( lim seq)).| < p by A6;

        reconsider N = n as Element of NAT by ORDINAL1:def 12;

        take N;

        hereby

          let m be Nat;

          assume N <= m;

          then

           A9: |.((seq . m) - ( lim seq)).| < p by A8;

          ((rseq . m) - g) = ((seq . m) - ( lim seq)) by A1, A5, SUPINF_2: 3;

          hence |.((rseq . m) - g) qua Complex.| < p by A9, EXTREAL1: 12;

        end;

      end;

      then rseq is convergent by SEQ_2:def 6;

      hence thesis by A5, A7, SEQ_2:def 7;

    end;

    theorem :: RINFSUP2:16

    

     Th16: (seq ^\ k) is convergent_to_finite_number implies seq is convergent_to_finite_number & seq is convergent & ( lim seq) = ( lim (seq ^\ k))

    proof

      set seq0 = (seq ^\ k);

      assume

       A1: (seq ^\ k) is convergent_to_finite_number;

      then

       A2: not (( lim seq0) = +infty & seq0 is convergent_to_+infty) by MESFUNC5: 50;

      

       A3: not (( lim seq0) = -infty & seq0 is convergent_to_-infty) by A1, MESFUNC5: 51;

      seq0 is convergent by A1, MESFUNC5:def 11;

      then

       A4: ex g be Real st ( lim seq0) = g & (for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq0 . m) - ( lim seq0)).| < p) & seq0 is convergent_to_finite_number by A2, A3, MESFUNC5:def 12;

      then

      consider g be Real such that

       A5: ( lim seq0) = g;

      

       A6: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - ( lim seq0)).| < p

      proof

        let p be Real;

        assume 0 < p;

        then

        consider n be Nat such that

         A7: for m be Nat st n <= m holds |.((seq0 . m) - ( lim seq0)).| < p by A4;

        take n1 = (n + k);

        hereby

          let m be Nat;

          assume

           A8: n1 <= m;

          k <= (n + k) by NAT_1: 11;

          then

          reconsider mk = (m - k) as Element of NAT by A8, INT_1: 5, XXREAL_0: 2;

          

           A9: (seq0 . (m - k)) = (seq . (mk + k)) by NAT_1:def 3;

          ((n + k) - k) <= (m - k) by A8, XREAL_1: 9;

          hence |.((seq . m) - ( lim seq0)).| < p by A7, A9;

        end;

      end;

      ( lim seq0) = g by A5;

      hence

       A10: seq is convergent_to_finite_number by A6, MESFUNC5:def 8;

      hence seq is convergent by MESFUNC5:def 11;

      hence thesis by A5, A6, A10, MESFUNC5:def 12;

    end;

    theorem :: RINFSUP2:17

    

     Th17: (seq ^\ k) is convergent implies seq is convergent & ( lim seq) = ( lim (seq ^\ k))

    proof

      set seq0 = (seq ^\ k);

      assume

       A1: (seq ^\ k) is convergent;

      per cases by A1, MESFUNC5:def 11;

        suppose seq0 is convergent_to_finite_number;

        hence thesis by Th16;

      end;

        suppose

         A2: seq0 is convergent_to_+infty;

        for g be Real st 0 < g holds ex n be Nat st for m be Nat st n <= m holds g <= (seq . m)

        proof

          let g be Real;

          assume 0 < g;

          then

          consider n be Nat such that

           A3: for m be Nat st n <= m holds g <= (seq0 . m) by A2, MESFUNC5:def 9;

          take n1 = (n + k);

          hereby

            let m be Nat;

            assume

             A4: n1 <= m;

            k <= (n + k) by NAT_1: 11;

            then

            reconsider mk = (m - k) as Element of NAT by A4, INT_1: 5, XXREAL_0: 2;

            

             A5: (seq0 . (m - k)) = (seq . (mk + k)) by NAT_1:def 3;

            ((n + k) - k) <= (m - k) by A4, XREAL_1: 9;

            hence g <= (seq . m) by A3, A5;

          end;

        end;

        then

         A6: seq is convergent_to_+infty by MESFUNC5:def 9;

        hence

         A7: seq is convergent by MESFUNC5:def 11;

        ( lim seq0) = +infty by A1, A2, MESFUNC5:def 12;

        hence thesis by A6, A7, MESFUNC5:def 12;

      end;

        suppose

         A8: seq0 is convergent_to_-infty;

        for g be Real st g < 0 holds ex n be Nat st for m be Nat st n <= m holds (seq . m) <= g

        proof

          let g be Real;

          assume g < 0 ;

          then

          consider n be Nat such that

           A9: for m be Nat st n <= m holds (seq0 . m) <= g by A8, MESFUNC5:def 10;

          take n1 = (n + k);

          hereby

            let m be Nat;

            assume

             A10: n1 <= m;

            k <= (n + k) by NAT_1: 11;

            then

            reconsider mk = (m - k) as Element of NAT by A10, INT_1: 5, XXREAL_0: 2;

            

             A11: (seq0 . (m - k)) = (seq . (mk + k)) by NAT_1:def 3;

            ((n + k) - k) <= (m - k) by A10, XREAL_1: 9;

            hence (seq . m) <= g by A9, A11;

          end;

        end;

        then

         A12: seq is convergent_to_-infty by MESFUNC5:def 10;

        hence

         A13: seq is convergent by MESFUNC5:def 11;

        ( lim seq0) = -infty by A1, A8, MESFUNC5:def 12;

        hence thesis by A12, A13, MESFUNC5:def 12;

      end;

    end;

    theorem :: RINFSUP2:18

    

     Th18: ( lim_sup seq) = ( lim_inf seq) & ( lim_inf seq) in REAL implies ex k st (seq ^\ k) is bounded

    proof

      assume that

       A1: ( lim_sup seq) = ( lim_inf seq) and

       A2: ( lim_inf seq) in REAL ;

      reconsider a = ( lim_inf seq) as Real by A2;

      set K1 = (a + 1);

      ex k1 be Element of NAT st (( superior_realsequence seq) . k1) <= K1

      proof

        assume

         A3: not ex k1 be Element of NAT st (( superior_realsequence seq) . k1) <= K1;

        now

          let x be ExtReal;

          assume x in ( rng ( superior_realsequence seq));

          then ex n be object st n in ( dom ( superior_realsequence seq)) & x = (( superior_realsequence seq) . n) by FUNCT_1:def 3;

          hence K1 <= x by A3;

        end;

        then K1 is LowerBound of ( rng ( superior_realsequence seq)) by XXREAL_2:def 2;

        then (a + 1) <= a by A1, XXREAL_2:def 4;

        hence contradiction by XREAL_1: 29;

      end;

      then

      consider k1 be Element of NAT such that

       A4: (( superior_realsequence seq) . k1) <= K1;

      set K2 = (a - 1);

      ex k2 be Element of NAT st K2 <= (( inferior_realsequence seq) . k2)

      proof

        assume

         A5: not (ex k2 be Element of NAT st K2 <= (( inferior_realsequence seq) . k2));

        now

          let x be ExtReal;

          assume x in ( rng ( inferior_realsequence seq));

          then ex n be object st n in ( dom ( inferior_realsequence seq)) & x = (( inferior_realsequence seq) . n) by FUNCT_1:def 3;

          hence x <= K2 by A5;

        end;

        then K2 is UpperBound of ( rng ( inferior_realsequence seq)) by XXREAL_2:def 1;

        then a <= (a - 1) by XXREAL_2:def 3;

        then (a + 0 ) < ((a - 1) + 1) by XREAL_1: 8;

        hence contradiction;

      end;

      then

      consider k2 be Element of NAT such that

       A6: K2 <= (( inferior_realsequence seq) . k2);

      take k = ( max (k1,k2));

      k2 <= k by XXREAL_0: 25;

      then (( inferior_realsequence seq) . k2) <= (( inferior_realsequence seq) . k) by Th7;

      then

       A7: K2 <= (( inferior_realsequence seq) . k) by A6, XXREAL_0: 2;

      k1 <= k by XXREAL_0: 25;

      then (( superior_realsequence seq) . k) <= (( superior_realsequence seq) . k1) by Th7;

      then

       A8: (( superior_realsequence seq) . k) <= K1 by A4, XXREAL_0: 2;

      

       A9: for n be Element of NAT st k <= n holds (seq . n) <= K1 & K2 <= (seq . n)

      proof

        let n be Element of NAT ;

        

         A10: (( inferior_realsequence seq) . n) <= (seq . n) by Th8;

        assume

         A11: k <= n;

        then (( superior_realsequence seq) . n) <= (( superior_realsequence seq) . k) by Th7;

        then

         A12: (( superior_realsequence seq) . n) <= K1 by A8, XXREAL_0: 2;

        (( inferior_realsequence seq) . k) <= (( inferior_realsequence seq) . n) by A11, Th7;

        then

         A13: K2 <= (( inferior_realsequence seq) . n) by A7, XXREAL_0: 2;

        (seq . n) <= (( superior_realsequence seq) . n) by Th8;

        hence thesis by A12, A13, A10, XXREAL_0: 2;

      end;

      now

        let x be ExtReal;

        assume x in ( rng (seq ^\ k));

        then

        consider n be object such that

         A14: n in ( dom (seq ^\ k)) and

         A15: x = ((seq ^\ k) . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A14;

        

         A16: k <= (n + k) by NAT_1: 11;

        x = (seq . (n + k)) by A15, NAT_1:def 3;

        hence x <= K1 by A9, A16;

      end;

      then K1 is UpperBound of ( rng (seq ^\ k)) by XXREAL_2:def 1;

      hence ( rng (seq ^\ k)) is bounded_above by XXREAL_2:def 10;

      now

        let x be ExtReal;

        assume x in ( rng (seq ^\ k));

        then

        consider n be object such that

         A17: n in ( dom (seq ^\ k)) and

         A18: x = ((seq ^\ k) . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A17;

        

         A19: k <= (n + k) by NAT_1: 11;

        x = (seq . (n + k)) by A18, NAT_1:def 3;

        hence K2 <= x by A9, A19;

      end;

      then K2 is LowerBound of ( rng (seq ^\ k)) by XXREAL_2:def 2;

      hence ( rng (seq ^\ k)) is bounded_below by XXREAL_2:def 9;

    end;

    theorem :: RINFSUP2:19

    

     Th19: seq is convergent_to_finite_number implies ex k st (seq ^\ k) is bounded

    proof

      assume

       A1: seq is convergent_to_finite_number;

      then

       A2: not (( lim seq) = +infty & seq is convergent_to_+infty) by MESFUNC5: 50;

      

       A3: not (( lim seq) = -infty & seq is convergent_to_-infty) by A1, MESFUNC5: 51;

      seq is convergent by A1, MESFUNC5:def 11;

      then

       A4: ex g be Real st ( lim seq) = g & (for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - ( lim seq)).| < p) & seq is convergent_to_finite_number by A2, A3, MESFUNC5:def 12;

      then

      consider g be Real such that

       A5: ( lim seq) = g;

      reconsider jj = 1 as Real;

      set UB = (g + jj);

      consider k be Nat such that

       A6: for m be Nat st k <= m holds |.((seq . m) - ( lim seq)).| < 1 by A4;

      reconsider K = k as Element of NAT by ORDINAL1:def 12;

      take K;

      now

        let r be ExtReal;

        assume r in ( rng (seq ^\ K));

        then

        consider n be object such that

         A7: n in ( dom (seq ^\ K)) and

         A8: r = ((seq ^\ K) . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A7;

         |.((seq . (n + k)) - ( lim seq)).| <= 1. by A6, NAT_1: 11;

        then ((seq . (n + k)) - ( lim seq)) <= 1. by EXTREAL1: 23;

        then (((seq . (n + k)) + ( - ( lim seq))) + ( lim seq)) <= ( 1. + ( lim seq)) by XXREAL_3: 36;

        then ((seq . (n + k)) + (( - ( lim seq)) + ( lim seq))) <= ( 1. + ( lim seq)) by A5, XXREAL_3: 29;

        then ((seq . (n + k)) + 0. ) <= ( 1. + ( lim seq)) by XXREAL_3: 7;

        then (seq . (n + k)) <= ( 1. + ( lim seq)) by XXREAL_3: 4;

        then (seq . (n + k)) <= UB by A5, SUPINF_2: 1;

        hence r <= UB by A8, NAT_1:def 3;

      end;

      then UB is UpperBound of ( rng (seq ^\ K)) by XXREAL_2:def 1;

      hence ( rng (seq ^\ K)) is bounded_above by XXREAL_2:def 10;

      set UL = (g - 1);

      now

        let r be ExtReal;

        assume r in ( rng (seq ^\ K));

        then

        consider n be object such that

         A9: n in ( dom (seq ^\ K)) and

         A10: r = ((seq ^\ K) . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A9;

         |.((seq . (n + k)) - ( lim seq)).| < 1 by A6, NAT_1: 11;

        then ( - 1. ) <= ((seq . (n + k)) - ( lim seq)) by EXTREAL1: 23;

        then (( - 1. ) + ( lim seq)) <= (((seq . (n + k)) + ( - ( lim seq))) + ( lim seq)) by XXREAL_3: 36;

        then (( - 1. ) + ( lim seq)) <= ((seq . (n + k)) + (( - ( lim seq)) + ( lim seq))) by A5, XXREAL_3: 29;

        then

         A11: (( - 1. ) + ( lim seq)) <= ((seq . (n + k)) + 0. ) by XXREAL_3: 7;

        ( - 1. ) = ( - jj) by SUPINF_2: 2;

        then (( - jj) + g) = (( - 1. ) + ( lim seq)) by A5, SUPINF_2: 1;

        then UL <= (seq . (n + k)) by A11, XXREAL_3: 4;

        hence UL <= r by A10, NAT_1:def 3;

      end;

      then UL is LowerBound of ( rng (seq ^\ K)) by XXREAL_2:def 2;

      hence ( rng (seq ^\ K)) is bounded_below by XXREAL_2:def 9;

    end;

    theorem :: RINFSUP2:20

    

     Th20: seq is convergent_to_finite_number implies (seq ^\ k) is convergent_to_finite_number & (seq ^\ k) is convergent & ( lim seq) = ( lim (seq ^\ k))

    proof

      set seq0 = (seq ^\ k);

      assume

       A1: seq is convergent_to_finite_number;

      then

       A2: not (( lim seq) = +infty & seq is convergent_to_+infty) by MESFUNC5: 50;

      

       A3: not (( lim seq) = -infty & seq is convergent_to_-infty) by A1, MESFUNC5: 51;

      seq is convergent by A1, MESFUNC5:def 11;

      then

       A4: ex g be Real st ( lim seq) = g & (for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - ( lim seq)).| < p) & seq is convergent_to_finite_number by A2, A3, MESFUNC5:def 12;

      then

      consider g be Real such that

       A5: ( lim seq) = g;

      

       A6: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq0 . m) - ( lim seq)).| < p

      proof

        let p be Real;

        assume 0 < p;

        then

        consider n be Nat such that

         A7: for m be Nat st n <= m holds |.((seq . m) - ( lim seq)).| < p by A4;

        take n;

        hereby

          let m be Nat such that

           A8: n <= m;

          m <= (m + k) by NAT_1: 11;

          then n <= (m + k) by A8, XXREAL_0: 2;

          then |.((seq . (m + k)) - ( lim seq)).| < p by A7;

          hence |.((seq0 . m) - ( lim seq)).| < p by NAT_1:def 3;

        end;

      end;

      ( lim seq) = g by A5;

      hence

       A9: seq0 is convergent_to_finite_number by A6, MESFUNC5:def 8;

      hence seq0 is convergent by MESFUNC5:def 11;

      hence thesis by A5, A6, A9, MESFUNC5:def 12;

    end;

    theorem :: RINFSUP2:21

    seq is convergent implies (seq ^\ k) is convergent & ( lim seq) = ( lim (seq ^\ k))

    proof

      set seq0 = (seq ^\ k);

      assume

       A1: seq is convergent;

      per cases by A1, MESFUNC5:def 11;

        suppose seq is convergent_to_finite_number;

        hence thesis by Th20;

      end;

        suppose

         A2: seq is convergent_to_+infty;

        for g be Real st 0 < g holds ex n be Nat st for m be Nat st n <= m holds g <= (seq0 . m)

        proof

          let g be Real;

          assume 0 < g;

          then

          consider n be Nat such that

           A3: for m be Nat st n <= m holds g <= (seq . m) by A2, MESFUNC5:def 9;

          take n;

          hereby

            let m be Nat such that

             A4: n <= m;

            m <= (m + k) by NAT_1: 11;

            then n <= (m + k) by A4, XXREAL_0: 2;

            then g <= (seq . (m + k)) by A3;

            hence g <= (seq0 . m) by NAT_1:def 3;

          end;

        end;

        then

         A5: seq0 is convergent_to_+infty by MESFUNC5:def 9;

        hence

         A6: seq0 is convergent by MESFUNC5:def 11;

        ( lim seq) = +infty by A1, A2, MESFUNC5:def 12;

        hence thesis by A5, A6, MESFUNC5:def 12;

      end;

        suppose

         A7: seq is convergent_to_-infty;

        for g be Real st g < 0 holds ex n be Nat st for m be Nat st n <= m holds (seq0 . m) <= g

        proof

          let g be Real;

          assume g < 0 ;

          then

          consider n be Nat such that

           A8: for m be Nat st n <= m holds (seq . m) <= g by A7, MESFUNC5:def 10;

          take n;

          hereby

            let m be Nat such that

             A9: n <= m;

            m <= (m + k) by NAT_1: 11;

            then n <= (m + k) by A9, XXREAL_0: 2;

            then (seq . (m + k)) <= g by A8;

            hence (seq0 . m) <= g by NAT_1:def 3;

          end;

        end;

        then

         A10: seq0 is convergent_to_-infty by MESFUNC5:def 10;

        hence

         A11: seq0 is convergent by MESFUNC5:def 11;

        ( lim seq) = -infty by A1, A7, MESFUNC5:def 12;

        hence thesis by A10, A11, MESFUNC5:def 12;

      end;

    end;

    theorem :: RINFSUP2:22

    (seq is bounded_above implies (seq ^\ k) is bounded_above) & (seq is bounded_below implies (seq ^\ k) is bounded_below)

    proof

      hereby

        assume seq is bounded_above;

        then ( rng seq) is bounded_above;

        then

        consider UB be Real such that

         A1: UB is UpperBound of ( rng seq) by XXREAL_2:def 10;

        now

          let r be ExtReal;

          assume r in ( rng (seq ^\ k));

          then

          consider n be object such that

           A2: n in ( dom (seq ^\ k)) and

           A3: r = ((seq ^\ k) . n) by FUNCT_1:def 3;

          reconsider n as Element of NAT by A2;

          (n + k) in NAT by ORDINAL1:def 12;

          then (seq . (n + k)) <= UB by A1, FUNCT_2: 4, XXREAL_2:def 1;

          hence r <= UB by A3, NAT_1:def 3;

        end;

        then UB is UpperBound of ( rng (seq ^\ k)) by XXREAL_2:def 1;

        then ( rng (seq ^\ k)) is bounded_above by XXREAL_2:def 10;

        hence (seq ^\ k) is bounded_above;

      end;

      hereby

        assume seq is bounded_below;

        then ( rng seq) is bounded_below;

        then

        consider UB be Real such that

         A4: UB is LowerBound of ( rng seq) by XXREAL_2:def 9;

        now

          let r be ExtReal;

          assume r in ( rng (seq ^\ k));

          then

          consider n be object such that

           A5: n in ( dom (seq ^\ k)) and

           A6: r = ((seq ^\ k) . n) by FUNCT_1:def 3;

          reconsider n as Element of NAT by A5;

          (n + k) in NAT by ORDINAL1:def 12;

          then (seq . (n + k)) in ( rng seq) by FUNCT_2: 4;

          then UB <= (seq . (n + k)) by A4, XXREAL_2:def 2;

          hence UB <= r by A6, NAT_1:def 3;

        end;

        then UB is LowerBound of ( rng (seq ^\ k)) by XXREAL_2:def 2;

        then ( rng (seq ^\ k)) is bounded_below by XXREAL_2:def 9;

        hence (seq ^\ k) is bounded_below;

      end;

    end;

    theorem :: RINFSUP2:23

    

     Th23: ( inf seq) <= (seq . n) & (seq . n) <= ( sup seq)

    proof

      

       A1: ( inf ( rng seq)) is LowerBound of ( rng seq) by XXREAL_2:def 4;

      

       A2: ( sup ( rng seq)) is UpperBound of ( rng seq) by XXREAL_2:def 3;

      n in NAT by ORDINAL1:def 12;

      then (seq . n) in ( rng seq) by FUNCT_2: 4;

      hence thesis by A1, A2, XXREAL_2:def 1, XXREAL_2:def 2;

    end;

    theorem :: RINFSUP2:24

    

     Th24: ( inf seq) <= ( sup seq)

    proof

      

       A1: (seq . 0 ) <= ( sup seq) by Th23;

      ( inf seq) <= (seq . 0 ) by Th23;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: RINFSUP2:25

    

     Th25: seq is non-increasing implies (seq ^\ k) is non-increasing & ( inf seq) = ( inf (seq ^\ k))

    proof

      set seq0 = (seq ^\ k);

      assume

       A1: seq is non-increasing;

      now

        let n,m be Nat;

        assume m <= n;

        then (k + m) <= (k + n) by XREAL_1: 6;

        then (seq . (k + n)) <= (seq . (k + m)) by A1, Th7;

        then (seq0 . n) <= (seq . (k + m)) by NAT_1:def 3;

        hence (seq0 . n) <= (seq0 . m) by NAT_1:def 3;

      end;

      hence (seq ^\ k) is non-increasing;

      now

        let y be ExtReal;

        assume y in ( rng seq);

        then

        consider n be object such that

         A2: n in ( dom seq) and

         A3: y = (seq . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A2;

        (seq0 . n) = (seq . (n + k)) by NAT_1:def 3;

        then

         A4: ( inf seq0) <= (seq . (n + k)) by Th23;

        n <= (n + k) by NAT_1: 11;

        then (seq . (n + k)) <= (seq . n) by A1, Th7;

        hence ( inf ( rng seq0)) <= y by A3, A4, XXREAL_0: 2;

      end;

      then ( inf ( rng seq0)) is LowerBound of ( rng seq) by XXREAL_2:def 2;

      then

       A5: ( inf ( rng seq0)) <= ( inf ( rng seq)) by XXREAL_2:def 4;

      now

        let y be ExtReal;

        assume y in ( rng seq0);

        then

        consider n be object such that

         A6: n in ( dom seq0) and

         A7: y = (seq0 . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A6;

        (seq0 . n) = (seq . (n + k)) by NAT_1:def 3;

        then ( inf seq) <= (seq0 . n) by Th23;

        hence ( inf ( rng seq)) <= y by A7;

      end;

      then ( inf ( rng seq)) is LowerBound of ( rng seq0) by XXREAL_2:def 2;

      then ( inf ( rng seq)) <= ( inf ( rng seq0)) by XXREAL_2:def 4;

      hence thesis by A5, XXREAL_0: 1;

    end;

    theorem :: RINFSUP2:26

    

     Th26: seq is non-decreasing implies (seq ^\ k) is non-decreasing & ( sup seq) = ( sup (seq ^\ k))

    proof

      set seq0 = (seq ^\ k);

      assume

       A1: seq is non-decreasing;

      now

        let n,m be Nat;

        assume m <= n;

        then (k + m) <= (k + n) by XREAL_1: 6;

        then (seq . (k + m)) <= (seq . (k + n)) by A1, Th7;

        then (seq0 . m) <= (seq . (k + n)) by NAT_1:def 3;

        hence (seq0 . m) <= (seq0 . n) by NAT_1:def 3;

      end;

      hence (seq ^\ k) is non-decreasing;

      now

        let y be ExtReal;

        assume y in ( rng seq);

        then

        consider n be object such that

         A2: n in ( dom seq) and

         A3: y = (seq . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A2;

        (seq0 . n) = (seq . (n + k)) by NAT_1:def 3;

        then

         A4: (seq . (n + k)) <= ( sup seq0) by Th23;

        n <= (n + k) by NAT_1: 11;

        then (seq . n) <= (seq . (n + k)) by A1, Th7;

        hence y <= ( sup ( rng seq0)) by A3, A4, XXREAL_0: 2;

      end;

      then ( sup ( rng seq0)) is UpperBound of ( rng seq) by XXREAL_2:def 1;

      then

       A5: ( sup ( rng seq)) <= ( sup ( rng seq0)) by XXREAL_2:def 3;

      now

        let y be ExtReal;

        assume y in ( rng seq0);

        then

        consider n be object such that

         A6: n in ( dom seq0) and

         A7: y = (seq0 . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A6;

        (seq0 . n) = (seq . (n + k)) by NAT_1:def 3;

        then (seq0 . n) <= ( sup seq) by Th23;

        hence y <= ( sup ( rng seq)) by A7;

      end;

      then ( sup ( rng seq)) is UpperBound of ( rng seq0) by XXREAL_2:def 1;

      then ( sup ( rng seq0)) <= ( sup ( rng seq)) by XXREAL_2:def 3;

      hence thesis by A5, XXREAL_0: 1;

    end;

    theorem :: RINFSUP2:27

    (( superior_realsequence seq) . n) = ( sup (seq ^\ n)) & (( inferior_realsequence seq) . n) = ( inf (seq ^\ n))

    proof

      set rseq = (seq ^\ n);

      

       A1: ex Z be non empty Subset of ExtREAL st Z = { (seq . k) : n <= k } & (( inferior_realsequence seq) . n) = ( inf Z) by Def6;

      now

        let x be object;

        assume x in { (seq . k) : n <= k };

        then

        consider k be Nat such that

         A2: x = (seq . k) and

         A3: n <= k;

        reconsider k1 = (k - n) as Element of NAT by A3, INT_1: 5;

        x = (seq . (n + k1)) by A2;

        then x = (rseq . k1) by NAT_1:def 3;

        hence x in ( rng rseq) by FUNCT_2: 4;

      end;

      then

       A4: { (seq . k) : n <= k } c= ( rng rseq);

      now

        let x be object;

        assume x in ( rng rseq);

        then

        consider z be object such that

         A5: z in ( dom rseq) and

         A6: x = (rseq . z) by FUNCT_1:def 3;

        reconsider k0 = z as Element of NAT by A5;

        

         A7: n <= (n + k0) by NAT_1: 11;

        x = (seq . (n + k0)) by A6, NAT_1:def 3;

        hence x in { (seq . k) : n <= k } by A7;

      end;

      then

       A8: ( rng rseq) c= { (seq . k) : n <= k };

      ex Y be non empty Subset of ExtREAL st Y = { (seq . k) : n <= k } & (( superior_realsequence seq) . n) = ( sup Y) by Def7;

      hence thesis by A1, A4, A8, XBOOLE_0:def 10;

    end;

    theorem :: RINFSUP2:28

    

     Th28: for seq be ExtREAL_sequence, j be Element of NAT holds ( superior_realsequence (seq ^\ j)) = (( superior_realsequence seq) ^\ j) & ( lim_sup (seq ^\ j)) = ( lim_sup seq)

    proof

      let seq be ExtREAL_sequence, j be Element of NAT ;

      set rseq = (seq ^\ j);

      now

        let n be Element of NAT ;

        

         A1: ex Y2 be non empty Subset of ExtREAL st Y2 = { (rseq . k) : n <= k } & (( superior_realsequence rseq) . n) = ( sup Y2) by Def7;

        

         A2: ex Y3 be non empty Subset of ExtREAL st Y3 = { (seq . k) : (j + n) <= k } & (( superior_realsequence seq) . (j + n)) = ( sup Y3) by Def7;

        now

          let x be object;

          assume x in { (seq . k) where k : (j + n) <= k };

          then

          consider k be Nat such that

           A3: x = (seq . k) and

           A4: (j + n) <= k;

          j <= (j + n) by NAT_1: 11;

          then

          reconsider k1 = (k - j) as Element of NAT by A4, INT_1: 5, XXREAL_0: 2;

          

           A5: x = (seq . (j + k1)) by A3;

          ((j + n) - j) <= (k - j) by A4, XREAL_1: 9;

          hence x in { (seq . (j + k2)) where k2 : n <= k2 } by A5;

        end;

        then

         A6: { (seq . k) where k : (j + n) <= k } c= { (seq . (j + k)) where k : n <= k };

        now

          let x be object;

          assume x in { (seq . (j + k)) where k : n <= k };

          then

          consider k be Nat such that

           A7: x = (seq . (j + k)) and

           A8: n <= k;

          (j + n) <= (j + k) by A8, XREAL_1: 6;

          hence x in { (seq . k1) where k1 : (j + n) <= k1 } by A7;

        end;

        then { (seq . (j + k)) where k : n <= k } c= { (seq . k) where k : (j + n) <= k };

        then

         A9: { (seq . (j + k)) where k : n <= k } = { (seq . k) where k : (j + n) <= k } by A6, XBOOLE_0:def 10;

        now

          let x be object;

          assume x in { (seq . (j + k)) where k : n <= k };

          then

          consider k be Nat such that

           A10: x = (seq . (j + k)) and

           A11: n <= k;

          x = (rseq . k) by A10, NAT_1:def 3;

          hence x in { (rseq . k1) where k1 : n <= k1 } by A11;

        end;

        then

         A12: { (seq . (j + k)) where k : n <= k } c= { (rseq . k) where k : n <= k };

        now

          let x be object;

          assume x in { (rseq . k) where k : n <= k };

          then

          consider k be Nat such that

           A13: x = (rseq . k) and

           A14: n <= k;

          x = (seq . (j + k)) by A13, NAT_1:def 3;

          hence x in { (seq . (j + k1)) where k1 : n <= k1 } by A14;

        end;

        then { (rseq . k) where k : n <= k } c= { (seq . (j + k)) where k : n <= k };

        then { (rseq . k) where k : n <= k } = { (seq . (j + k)) where k : n <= k } by A12, XBOOLE_0:def 10;

        hence (( superior_realsequence rseq) . n) = ((( superior_realsequence seq) ^\ j) . n) by A1, A2, A9, NAT_1:def 3;

      end;

      then (( superior_realsequence seq) ^\ j) = ( superior_realsequence rseq) by FUNCT_2: 63;

      hence thesis by Th25;

    end;

    theorem :: RINFSUP2:29

    

     Th29: for seq be ExtREAL_sequence, j be Element of NAT holds ( inferior_realsequence (seq ^\ j)) = (( inferior_realsequence seq) ^\ j) & ( lim_inf (seq ^\ j)) = ( lim_inf seq)

    proof

      let seq be ExtREAL_sequence, j be Element of NAT ;

      set rseq = (seq ^\ j);

      now

        let n be Element of NAT ;

        

         A1: ex Y2 be non empty Subset of ExtREAL st Y2 = { (rseq . k) : n <= k } & (( inferior_realsequence rseq) . n) = ( inf Y2) by Def6;

        

         A2: ex Y3 be non empty Subset of ExtREAL st Y3 = { (seq . k) : (j + n) <= k } & (( inferior_realsequence seq) . (j + n)) = ( inf Y3) by Def6;

        now

          let x be object;

          assume x in { (seq . k) where k : (j + n) <= k };

          then

          consider k be Nat such that

           A3: x = (seq . k) and

           A4: (j + n) <= k;

          j <= (j + n) by NAT_1: 11;

          then

          reconsider k1 = (k - j) as Element of NAT by A4, INT_1: 5, XXREAL_0: 2;

          

           A5: x = (seq . (j + k1)) by A3;

          ((j + n) - j) <= (k - j) by A4, XREAL_1: 9;

          hence x in { (seq . (j + k2)) where k2 : n <= k2 } by A5;

        end;

        then

         A6: { (seq . k) where k : (j + n) <= k } c= { (seq . (j + k)) where k : n <= k };

        now

          let x be object;

          assume x in { (seq . (j + k)) where k : n <= k };

          then

          consider k be Nat such that

           A7: x = (seq . (j + k)) and

           A8: n <= k;

          (j + n) <= (j + k) by A8, XREAL_1: 6;

          hence x in { (seq . k1) where k1 : (j + n) <= k1 } by A7;

        end;

        then { (seq . (j + k)) where k : n <= k } c= { (seq . k) where k : (j + n) <= k };

        then

         A9: { (seq . (j + k)) where k : n <= k } = { (seq . k) where k : (j + n) <= k } by A6, XBOOLE_0:def 10;

        now

          let x be object;

          assume x in { (seq . (j + k)) where k : n <= k };

          then

          consider k be Nat such that

           A10: x = (seq . (j + k)) and

           A11: n <= k;

          x = (rseq . k) by A10, NAT_1:def 3;

          hence x in { (rseq . k1) where k1 : n <= k1 } by A11;

        end;

        then

         A12: { (seq . (j + k)) where k : n <= k } c= { (rseq . k) where k : n <= k };

        now

          let x be object;

          assume x in { (rseq . k) where k : n <= k };

          then

          consider k be Nat such that

           A13: x = (rseq . k) and

           A14: n <= k;

          x = (seq . (j + k)) by A13, NAT_1:def 3;

          hence x in { (seq . (j + k1)) where k1 : n <= k1 } by A14;

        end;

        then { (rseq . k) where k : n <= k } c= { (seq . (j + k)) where k : n <= k };

        then { (rseq . k) where k : n <= k } = { (seq . (j + k)) where k : n <= k } by A12, XBOOLE_0:def 10;

        hence (( inferior_realsequence rseq) . n) = ((( inferior_realsequence seq) ^\ j) . n) by A1, A2, A9, NAT_1:def 3;

      end;

      then (( inferior_realsequence seq) ^\ j) = ( inferior_realsequence rseq) by FUNCT_2: 63;

      hence thesis by Th26;

    end;

    theorem :: RINFSUP2:30

    

     Th30: for seq be ExtREAL_sequence, k be Element of NAT st seq is non-increasing & -infty < (seq . k) & (seq . k) < +infty holds (seq ^\ k) is bounded_above & ( sup (seq ^\ k)) = (seq . k)

    proof

      let seq be ExtREAL_sequence, k be Element of NAT ;

      assume that

       A1: seq is non-increasing and

       A2: -infty < (seq . k) and

       A3: (seq . k) < +infty ;

      set seq0 = (seq ^\ k);

      now

        let y be ExtReal;

        assume y in ( rng seq0);

        then

        consider n be object such that

         A4: n in ( dom seq0) and

         A5: y = (seq0 . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A4;

        k <= (n + k) by NAT_1: 11;

        then (seq . (n + k)) <= (seq . k) by A1, Th7;

        hence y <= (seq . k) by A5, NAT_1:def 3;

      end;

      then

       A6: (seq . k) is UpperBound of ( rng seq0) by XXREAL_2:def 1;

      (seq0 . 0 ) = (seq . ( 0 + k)) by NAT_1:def 3;

      then

       A7: (seq . k) in ( rng seq0) by FUNCT_2: 4;

      (seq . k) in REAL by A2, A3, XXREAL_0: 14;

      then ( rng seq0) is bounded_above by A6, XXREAL_2:def 10;

      hence thesis by A6, A7, XXREAL_2: 55;

    end;

    theorem :: RINFSUP2:31

    

     Th31: for seq be ExtREAL_sequence, k be Element of NAT st seq is non-decreasing & -infty < (seq . k) & (seq . k) < +infty holds (seq ^\ k) is bounded_below & ( inf (seq ^\ k)) = (seq . k)

    proof

      let seq be ExtREAL_sequence, k be Element of NAT ;

      assume that

       A1: seq is non-decreasing and

       A2: -infty < (seq . k) and

       A3: (seq . k) < +infty ;

      set seq0 = (seq ^\ k);

      now

        let y be ExtReal;

        assume y in ( rng seq0);

        then

        consider n be object such that

         A4: n in ( dom seq0) and

         A5: y = (seq0 . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A4;

        k <= (n + k) by NAT_1: 11;

        then (seq . k) <= (seq . (n + k)) by A1, Th7;

        hence (seq . k) <= y by A5, NAT_1:def 3;

      end;

      then

       A6: (seq . k) is LowerBound of ( rng seq0) by XXREAL_2:def 2;

      (seq0 . 0 ) = (seq . ( 0 + k)) by NAT_1:def 3;

      then

       A7: (seq . k) in ( rng seq0) by FUNCT_2: 4;

      (seq . k) in REAL by A2, A3, XXREAL_0: 14;

      then ( rng seq0) is bounded_below by A6, XXREAL_2:def 9;

      hence thesis by A6, A7, XXREAL_2: 56;

    end;

    

     Lm3: for seq be ExtREAL_sequence st seq is bounded & seq is non-increasing holds seq is convergent_to_finite_number & seq is convergent & ( lim seq) = ( inf seq)

    proof

      let seq be ExtREAL_sequence;

      assume that

       A1: seq is bounded and

       A2: seq is non-increasing;

      reconsider rseq = seq as Real_Sequence by A1, Th11;

      

       A3: seq is bounded_below by A1;

      then

       A4: rseq is bounded_below by Th13;

      then ( lim rseq) = ( lim_sup rseq) by A2, RINFSUP1: 89;

      then ( lim rseq) = ( lower_bound rseq) by A2, RINFSUP1: 70;

      then

       A5: ( lim seq) = ( lower_bound rseq) by A2, A4, Th14;

      ( rng seq) is bounded_below by A3;

      hence thesis by A2, A4, A5, Th3, Th14;

    end;

    

     Lm4: for seq be ExtREAL_sequence st seq is bounded & seq is non-decreasing holds seq is convergent_to_finite_number & seq is convergent & ( lim seq) = ( sup seq)

    proof

      let seq be ExtREAL_sequence;

      assume that

       A1: seq is bounded and

       A2: seq is non-decreasing;

      reconsider rseq = seq as Real_Sequence by A1, Th11;

      

       A3: seq is bounded_above by A1;

      then

       A4: rseq is bounded_above by Th12;

      then ( lim rseq) = ( lim_inf rseq) by A2, RINFSUP1: 89;

      then ( lim rseq) = ( upper_bound rseq) by A2, RINFSUP1: 64;

      then

       A5: ( lim seq) = ( upper_bound rseq) by A2, A4, Th14;

      ( rng seq) is bounded_above by A3;

      hence thesis by A2, A4, A5, Th1, Th14;

    end;

    theorem :: RINFSUP2:32

    

     Th32: for seq be ExtREAL_sequence st (for n be Element of NAT holds +infty <= (seq . n)) holds seq is convergent_to_+infty

    proof

      let seq be ExtREAL_sequence;

      assume

       A1: for n be Element of NAT holds +infty <= (seq . n);

      now

        let g be Real;

        assume 0 < g;

        now

          let m be Nat;

          assume 0 <= m;

          m is Element of NAT by ORDINAL1:def 12;

          then

           A2: +infty <= (seq . m) by A1;

          g <= +infty by XXREAL_0: 3;

          hence g <= (seq . m) by A2, XXREAL_0: 2;

        end;

        hence ex n be Nat st for m be Nat st n <= m holds g <= (seq . m);

      end;

      hence thesis by MESFUNC5:def 9;

    end;

    theorem :: RINFSUP2:33

    

     Th33: for seq be ExtREAL_sequence st (for n be Element of NAT holds (seq . n) <= -infty ) holds seq is convergent_to_-infty

    proof

      let seq be ExtREAL_sequence;

      assume

       A1: for n be Element of NAT holds (seq . n) <= -infty ;

      now

        let g be Real;

        assume g < 0 ;

        now

          let m be Nat;

          assume 0 <= m;

          m is Element of NAT by ORDINAL1:def 12;

          then

           A2: (seq . m) <= -infty by A1;

           -infty <= g by XXREAL_0: 5;

          hence (seq . m) <= g by A2, XXREAL_0: 2;

        end;

        hence ex n be Nat st for m be Nat st n <= m holds (seq . m) <= g;

      end;

      hence thesis by MESFUNC5:def 10;

    end;

    theorem :: RINFSUP2:34

    

     Th34: for seq be ExtREAL_sequence st seq is non-increasing & -infty = ( inf seq) holds seq is convergent_to_-infty & ( lim seq) = -infty

    proof

      let seq be ExtREAL_sequence;

      assume that

       A1: seq is non-increasing and

       A2: -infty = ( inf seq);

      

       A3: seq is convergent_to_-infty

      proof

        assume not seq is convergent_to_-infty;

        then

        consider g be Real such that g < 0 and

         A4: for n be Nat holds ex m be Nat st n <= m & g < (seq . m) by MESFUNC5:def 10;

        for y be ExtReal st y in ( rng seq) holds g <= y

        proof

          let y be ExtReal;

          assume y in ( rng seq);

          then

          consider n be object such that

           A5: n in NAT and

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

          reconsider n as Element of NAT by A5;

          consider m be Nat such that

           A7: n <= m and

           A8: g < (seq . m) by A4;

          (seq . m) <= (seq . n) by A1, A7, Th7;

          hence thesis by A6, A8, XXREAL_0: 2;

        end;

        then g is LowerBound of ( rng seq) by XXREAL_2:def 2;

        then

         A9: g <= ( inf ( rng seq)) by XXREAL_2:def 4;

        g in REAL by XREAL_0:def 1;

        hence contradiction by A2, A9, XXREAL_0: 12;

      end;

      then seq is convergent by MESFUNC5:def 11;

      hence thesis by A3, MESFUNC5:def 12;

    end;

    theorem :: RINFSUP2:35

    

     Th35: for seq be ExtREAL_sequence st seq is non-decreasing & +infty = ( sup seq) holds seq is convergent_to_+infty & ( lim seq) = +infty

    proof

      let seq be ExtREAL_sequence;

      assume that

       A1: seq is non-decreasing and

       A2: +infty = ( sup seq);

      

       A3: seq is convergent_to_+infty

      proof

        assume not seq is convergent_to_+infty;

        then

        consider g be Real such that 0 < g and

         A4: for n be Nat holds ex m be Nat st n <= m & (seq . m) < g by MESFUNC5:def 9;

        for y be ExtReal st y in ( rng seq) holds y <= g

        proof

          let y be ExtReal;

          assume y in ( rng seq);

          then

          consider n be object such that

           A5: n in NAT and

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

          reconsider n as Element of NAT by A5;

          consider m be Nat such that

           A7: n <= m and

           A8: (seq . m) < g by A4;

          (seq . n) <= (seq . m) by A1, A7, Th7;

          hence thesis by A6, A8, XXREAL_0: 2;

        end;

        then g is UpperBound of ( rng seq) by XXREAL_2:def 1;

        then

         A9: ( sup ( rng seq)) <= g by XXREAL_2:def 3;

        g in REAL by XREAL_0:def 1;

        hence contradiction by A2, A9, XXREAL_0: 9;

      end;

      then seq is convergent by MESFUNC5:def 11;

      hence thesis by A3, MESFUNC5:def 12;

    end;

    theorem :: RINFSUP2:36

    

     Th36: for seq be ExtREAL_sequence st seq is non-increasing holds seq is convergent & ( lim seq) = ( inf seq)

    proof

      let seq be ExtREAL_sequence;

      assume

       A1: seq is non-increasing;

      per cases ;

        suppose

         A2: for n be Element of NAT holds +infty <= (seq . n);

        now

          let y be object;

          assume y in { +infty };

          then

           A3: y = +infty by TARSKI:def 1;

          now

            assume

             A4: not y in ( rng seq);

            now

              let n be Element of NAT ;

              n in NAT ;

              then n in ( dom seq) by FUNCT_2:def 1;

              then (seq . n) <> +infty by A3, A4, FUNCT_1:def 3;

              hence contradiction by A2, XXREAL_0: 4;

            end;

            hence contradiction;

          end;

          hence y in ( rng seq);

        end;

        then

         A5: { +infty } c= ( rng seq);

        

         A6: seq is convergent_to_+infty by A2, Th32;

        hence

         A7: seq is convergent by MESFUNC5:def 11;

        now

          let y be object;

          assume y in ( rng seq);

          then ex x be object st x in ( dom seq) & (seq . x) = y by FUNCT_1:def 3;

          then y = +infty by A2, XXREAL_0: 4;

          hence y in { +infty } by TARSKI:def 1;

        end;

        then ( rng seq) c= { +infty };

        then ( rng seq) = { +infty } by A5, XBOOLE_0:def 10;

        then ( inf seq) = +infty by XXREAL_2: 13;

        hence thesis by A6, A7, MESFUNC5:def 12;

      end;

        suppose not (for n be Element of NAT holds +infty <= (seq . n));

        then

        consider k be Element of NAT such that

         A8: (seq . k) < +infty ;

        per cases ;

          suppose

           A9: -infty <> ( inf seq);

          set seq0 = (seq ^\ k);

          

           A10: ( inf seq) = ( inf seq0) by A1, Th25;

           A11:

          now

            assume ( rng seq0) = { -infty };

            then

             A12: -infty in ( rng seq0) by TARSKI:def 1;

             -infty is LowerBound of ( rng seq0) by XXREAL_2: 42;

            hence contradiction by A9, A10, A12, XXREAL_2: 56;

          end;

          

           A13: ( inf seq0) <= ( sup seq0) by Th24;

          

           A14: ( inf ( rng seq0)) is LowerBound of ( rng seq0) by XXREAL_2:def 4;

          ( inf seq) <= (seq . k) by Th23;

          then -infty < (seq . k) by A9, XXREAL_0: 2, XXREAL_0: 6;

          then

           A15: seq0 is bounded_above by A1, A8, Th30;

          then ( rng seq0) is bounded_above;

          then ( sup ( rng seq0)) < +infty by A11, XXREAL_0: 9, XXREAL_2: 57;

          then ( inf ( rng seq0)) in REAL by A9, A10, A13, XXREAL_0: 14;

          then ( rng seq0) is bounded_below by A14, XXREAL_2:def 9;

          then seq0 is bounded_below;

          then

           A16: seq0 is bounded by A15;

          

           A17: seq0 is non-increasing by A1, Th25;

          then

           A18: ( lim seq0) = ( inf seq0) by A16, Lm3;

          seq0 is convergent by A17, A16, Lm3;

          hence thesis by A10, A18, Th17;

        end;

          suppose

           A19: -infty = ( inf seq);

          then seq is convergent_to_-infty by A1, Th34;

          hence seq is convergent by MESFUNC5:def 11;

          thus thesis by A1, A19, Th34;

        end;

      end;

    end;

    theorem :: RINFSUP2:37

    

     Th37: for seq be ExtREAL_sequence st seq is non-decreasing holds seq is convergent & ( lim seq) = ( sup seq)

    proof

      let seq be ExtREAL_sequence;

      assume

       A1: seq is non-decreasing;

      per cases ;

        suppose

         A2: for n be Element of NAT holds (seq . n) <= -infty ;

        now

          let y be object;

          assume y in { -infty };

          then

           A3: y = -infty by TARSKI:def 1;

          now

            assume

             A4: not y in ( rng seq);

            now

              let n be Element of NAT ;

              n in NAT ;

              then n in ( dom seq) by FUNCT_2:def 1;

              then (seq . n) <> -infty by A3, A4, FUNCT_1:def 3;

              hence contradiction by A2, XXREAL_0: 6;

            end;

            hence contradiction;

          end;

          hence y in ( rng seq);

        end;

        then

         A5: { -infty } c= ( rng seq);

        

         A6: seq is convergent_to_-infty by A2, Th33;

        hence

         A7: seq is convergent by MESFUNC5:def 11;

        now

          let y be object;

          assume y in ( rng seq);

          then ex x be object st x in ( dom seq) & (seq . x) = y by FUNCT_1:def 3;

          then y = -infty by A2, XXREAL_0: 6;

          hence y in { -infty } by TARSKI:def 1;

        end;

        then ( rng seq) c= { -infty };

        then ( rng seq) = { -infty } by A5, XBOOLE_0:def 10;

        then ( sup seq) = -infty by XXREAL_2: 11;

        hence thesis by A6, A7, MESFUNC5:def 12;

      end;

        suppose not (for n be Element of NAT holds (seq . n) <= -infty );

        then

        consider k be Element of NAT such that

         A8: -infty < (seq . k);

        per cases ;

          suppose

           A9: +infty <> ( sup seq);

          set seq0 = (seq ^\ k);

          

           A10: ( sup seq) = ( sup seq0) by A1, Th26;

           A11:

          now

            assume ( rng seq0) = { +infty };

            then

             A12: +infty in ( rng seq0) by TARSKI:def 1;

             +infty is UpperBound of ( rng seq0) by XXREAL_2: 41;

            hence contradiction by A9, A10, A12, XXREAL_2: 55;

          end;

          

           A13: ( inf seq0) <= ( sup seq0) by Th24;

          

           A14: ( sup ( rng seq0)) is UpperBound of ( rng seq0) by XXREAL_2:def 3;

          (seq . k) <= ( sup seq) by Th23;

          then (seq . k) < +infty by A9, XXREAL_0: 2, XXREAL_0: 4;

          then

           A15: seq0 is bounded_below by A1, A8, Th31;

          then ( rng seq0) is bounded_below;

          then -infty < ( inf ( rng seq0)) by A11, XXREAL_0: 12, XXREAL_2: 58;

          then ( sup ( rng seq0)) in REAL by A9, A10, A13, XXREAL_0: 14;

          then ( rng seq0) is bounded_above by A14, XXREAL_2:def 10;

          then seq0 is bounded_above;

          then

           A16: seq0 is bounded by A15;

          

           A17: seq0 is non-decreasing by A1, Th26;

          then

           A18: ( lim seq0) = ( sup seq0) by A16, Lm4;

          seq0 is convergent by A17, A16, Lm4;

          hence thesis by A10, A18, Th17;

        end;

          suppose

           A19: +infty = ( sup seq);

          then seq is convergent_to_+infty by A1, Th35;

          hence seq is convergent by MESFUNC5:def 11;

          thus thesis by A1, A19, Th35;

        end;

      end;

    end;

    theorem :: RINFSUP2:38

    

     Th38: for seq1,seq2 be ExtREAL_sequence st seq1 is convergent & seq2 is convergent & (for n holds (seq1 . n) <= (seq2 . n)) holds ( lim seq1) <= ( lim seq2)

    proof

      let seq1,seq2 be ExtREAL_sequence;

      assume that

       A1: seq1 is convergent and

       A2: seq2 is convergent and

       A3: for n holds (seq1 . n) <= (seq2 . n);

      per cases by A1, MESFUNC5:def 11;

        suppose

         A4: seq1 is convergent_to_finite_number;

        

         A5: not seq2 is convergent_to_-infty

        proof

          assume

           A6: seq2 is convergent_to_-infty;

          now

            let g be Real;

            assume g < 0 ;

            then

            consider n be Nat such that

             A7: for m be Nat st n <= m holds (seq2 . m) <= g by A6, MESFUNC5:def 10;

            now

              let m be Nat;

              

               A8: (seq1 . m) <= (seq2 . m) by A3;

              assume n <= m;

              then (seq2 . m) <= g by A7;

              hence (seq1 . m) <= g by A8, XXREAL_0: 2;

            end;

            hence ex n be Nat st for m be Nat st n <= m holds (seq1 . m) <= g;

          end;

          then seq1 is convergent_to_-infty by MESFUNC5:def 10;

          hence contradiction by A4, MESFUNC5: 51;

        end;

        per cases by A2, A5, MESFUNC5:def 11;

          suppose

           A9: seq2 is convergent_to_finite_number;

          consider k1 be Nat such that

           A10: (seq1 ^\ k1) is bounded by A4, Th19;

          (seq1 ^\ k1) is bounded_above by A10;

          then ( rng (seq1 ^\ k1)) is bounded_above;

          then

          consider UB be Real such that

           A11: UB is UpperBound of ( rng (seq1 ^\ k1)) by XXREAL_2:def 10;

          consider k2 be Nat such that

           A12: (seq2 ^\ k2) is bounded by A9, Th19;

          reconsider k = ( max (k1,k2)) as Element of NAT by ORDINAL1:def 12;

          

           A13: ( lim seq2) = ( lim (seq2 ^\ k)) by A9, Th20;

          

           A14: ( dom (seq1 ^\ k1)) = NAT by FUNCT_2:def 1;

          now

            reconsider k2 = (k - k1) as Element of NAT by INT_1: 5, XXREAL_0: 25;

            let y be object;

            assume y in ( rng (seq1 ^\ k));

            then

            consider n be object such that

             A15: n in ( dom (seq1 ^\ k)) and

             A16: ((seq1 ^\ k) . n) = y by FUNCT_1:def 3;

            reconsider n as Element of NAT by A15;

            y = (seq1 . (k + n)) by A16, NAT_1:def 3;

            then y = (seq1 . (k1 + (k2 + n)));

            then y = ((seq1 ^\ k1) . (k2 + n)) by NAT_1:def 3;

            hence y in ( rng (seq1 ^\ k1)) by A14, FUNCT_1:def 3;

          end;

          then

           A17: ( rng (seq1 ^\ k)) c= ( rng (seq1 ^\ k1));

          then UB is UpperBound of ( rng (seq1 ^\ k)) by A11, XXREAL_2: 6;

          then ( rng (seq1 ^\ k)) is bounded_above by XXREAL_2:def 10;

          then

           A18: (seq1 ^\ k) is bounded_above;

          (seq1 ^\ k1) is bounded_below by A10;

          then ( rng (seq1 ^\ k1)) is bounded_below;

          then

          consider LB be Real such that

           A19: LB is LowerBound of ( rng (seq1 ^\ k1)) by XXREAL_2:def 9;

          LB is LowerBound of ( rng (seq1 ^\ k)) by A17, A19, XXREAL_2: 5;

          then ( rng (seq1 ^\ k)) is bounded_below by XXREAL_2:def 9;

          then (seq1 ^\ k) is bounded_below;

          then (seq1 ^\ k) is bounded by A18;

          then

          reconsider rseq1 = (seq1 ^\ k) as Real_Sequence by Th11;

          (seq2 ^\ k2) is bounded_below by A12;

          then ( rng (seq2 ^\ k2)) is bounded_below;

          then

          consider LB be Real such that

           A20: LB is LowerBound of ( rng (seq2 ^\ k2)) by XXREAL_2:def 9;

          

           A21: ( lim seq1) = ( lim (seq1 ^\ k)) by A4, Th20;

          (seq2 ^\ k2) is bounded_above by A12;

          then ( rng (seq2 ^\ k2)) is bounded_above;

          then

          consider UB be Real such that

           A22: UB is UpperBound of ( rng (seq2 ^\ k2)) by XXREAL_2:def 10;

          

           A23: ( dom (seq2 ^\ k2)) = NAT by FUNCT_2:def 1;

          now

            reconsider k3 = (k - k2) as Element of NAT by INT_1: 5, XXREAL_0: 25;

            let y be object;

            assume y in ( rng (seq2 ^\ k));

            then

            consider n be object such that

             A24: n in ( dom (seq2 ^\ k)) and

             A25: ((seq2 ^\ k) . n) = y by FUNCT_1:def 3;

            reconsider n as Element of NAT by A24;

            y = (seq2 . (k + n)) by A25, NAT_1:def 3;

            then y = (seq2 . (k2 + (k3 + n)));

            then y = ((seq2 ^\ k2) . (k3 + n)) by NAT_1:def 3;

            hence y in ( rng (seq2 ^\ k2)) by A23, FUNCT_1:def 3;

          end;

          then

           A26: ( rng (seq2 ^\ k)) c= ( rng (seq2 ^\ k2));

          then UB is UpperBound of ( rng (seq2 ^\ k)) by A22, XXREAL_2: 6;

          then ( rng (seq2 ^\ k)) is bounded_above by XXREAL_2:def 10;

          then

           A27: (seq2 ^\ k) is bounded_above;

          LB is LowerBound of ( rng (seq2 ^\ k)) by A20, A26, XXREAL_2: 5;

          then ( rng (seq2 ^\ k)) is bounded_below by XXREAL_2:def 9;

          then (seq2 ^\ k) is bounded_below;

          then (seq2 ^\ k) is bounded by A27;

          then

          reconsider rseq2 = (seq2 ^\ k) as Real_Sequence by Th11;

          

           A28: (seq2 ^\ k) is convergent_to_finite_number by A9, Th20;

          then

           A29: rseq2 is convergent by Th15;

          

           A30: for n holds (rseq1 . n) <= (rseq2 . n)

          proof

            let n;

            

             A31: ((seq2 ^\ k) . n) = (seq2 . (k + n)) by NAT_1:def 3;

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

            hence thesis by A3, A31;

          end;

          

           A32: (seq1 ^\ k) is convergent_to_finite_number by A4, Th20;

          then

           A33: ( lim (seq1 ^\ k)) = ( lim rseq1) by Th15;

          

           A34: ( lim (seq2 ^\ k)) = ( lim rseq2) by A28, Th15;

          rseq1 is convergent by A32, Th15;

          hence thesis by A29, A33, A34, A30, A21, A13, SEQ_2: 18;

        end;

          suppose

           A35: seq2 is convergent_to_+infty;

          then seq2 is convergent by MESFUNC5:def 11;

          then ( lim seq2) = +infty by A35, MESFUNC5:def 12;

          hence thesis by XXREAL_0: 3;

        end;

      end;

        suppose

         A36: seq1 is convergent_to_+infty;

        now

          let g be Real;

          assume 0 < g;

          then

          consider n be Nat such that

           A37: for m be Nat st n <= m holds g <= (seq1 . m) by A36, MESFUNC5:def 9;

          now

            let m be Nat;

            

             A38: (seq1 . m) <= (seq2 . m) by A3;

            assume n <= m;

            then g <= (seq1 . m) by A37;

            hence g <= (seq2 . m) by A38, XXREAL_0: 2;

          end;

          hence ex n be Nat st for m be Nat st n <= m holds g <= (seq2 . m);

        end;

        then

         A39: seq2 is convergent_to_+infty by MESFUNC5:def 9;

        then seq2 is convergent by MESFUNC5:def 11;

        then ( lim seq2) = +infty by A39, MESFUNC5:def 12;

        hence thesis by XXREAL_0: 3;

      end;

        suppose

         A40: seq1 is convergent_to_-infty;

        then seq1 is convergent by MESFUNC5:def 11;

        then ( lim seq1) = -infty by A40, MESFUNC5:def 12;

        hence thesis by XXREAL_0: 5;

      end;

    end;

    theorem :: RINFSUP2:39

    for seq be ExtREAL_sequence holds ( lim_inf seq) <= ( lim_sup seq)

    proof

      let seq be ExtREAL_sequence;

      

       A1: ( lim ( superior_realsequence seq)) = ( lim_sup seq) by Th36;

      

       A2: ( inferior_realsequence seq) is convergent by Th37;

       A3:

      now

        let n be Nat;

        

         A4: (seq . n) <= (( superior_realsequence seq) . n) by Th8;

        (( inferior_realsequence seq) . n) <= (seq . n) by Th8;

        hence (( inferior_realsequence seq) . n) <= (( superior_realsequence seq) . n) by A4, XXREAL_0: 2;

      end;

      

       A5: ( lim ( inferior_realsequence seq)) = ( lim_inf seq) by Th37;

      ( superior_realsequence seq) is convergent by Th36;

      hence thesis by A1, A2, A5, A3, Th38;

    end;

    

     Lm5: for seq be ExtREAL_sequence st ( lim_inf seq) = ( lim_sup seq) & ( lim_inf seq) = +infty holds seq is convergent & ( lim seq) = ( lim_inf seq) & ( lim seq) = ( lim_sup seq)

    proof

      let seq be ExtREAL_sequence;

      assume that

       A1: ( lim_inf seq) = ( lim_sup seq) and

       A2: ( lim_inf seq) = +infty ;

      

       A3: ( inferior_realsequence seq) is convergent_to_+infty by A2, Th35;

      now

        let g be Real;

        assume 0 < g;

        then

        consider n be Nat such that

         A4: for m be Nat st n <= m holds g <= (( inferior_realsequence seq) . m) by A3, MESFUNC5:def 9;

        now

          let m be Nat;

          

           A5: (( inferior_realsequence seq) . m) <= (seq . m) by Th8;

          assume n <= m;

          then g <= (( inferior_realsequence seq) . m) by A4;

          hence g <= (seq . m) by A5, XXREAL_0: 2;

        end;

        hence ex n be Nat st for m be Nat st n <= m holds g <= (seq . m);

      end;

      then

       A6: seq is convergent_to_+infty by MESFUNC5:def 9;

      then seq is convergent by MESFUNC5:def 11;

      hence thesis by A1, A2, A6, MESFUNC5:def 12;

    end;

    

     Lm6: for seq be ExtREAL_sequence st ( lim_inf seq) = ( lim_sup seq) & ( lim_inf seq) = -infty holds seq is convergent & ( lim seq) = ( lim_inf seq) & ( lim seq) = ( lim_sup seq)

    proof

      let seq be ExtREAL_sequence;

      assume that

       A1: ( lim_inf seq) = ( lim_sup seq) and

       A2: ( lim_inf seq) = -infty ;

      

       A3: ( superior_realsequence seq) is convergent_to_-infty by A1, A2, Th34;

      now

        let g be Real;

        assume g < 0 ;

        then

        consider n be Nat such that

         A4: for m be Nat st n <= m holds (( superior_realsequence seq) . m) <= g by A3, MESFUNC5:def 10;

        now

          let m be Nat;

          

           A5: (seq . m) <= (( superior_realsequence seq) . m) by Th8;

          assume n <= m;

          then (( superior_realsequence seq) . m) <= g by A4;

          hence (seq . m) <= g by A5, XXREAL_0: 2;

        end;

        hence ex n be Nat st for m be Nat st n <= m holds (seq . m) <= g;

      end;

      then

       A6: seq is convergent_to_-infty by MESFUNC5:def 10;

      then seq is convergent by MESFUNC5:def 11;

      hence thesis by A1, A2, A6, MESFUNC5:def 12;

    end;

    

     Lm7: for seq be ExtREAL_sequence st ( lim_inf seq) = ( lim_sup seq) & ( lim_inf seq) in REAL holds seq is convergent & ( lim seq) = ( lim_inf seq) & ( lim seq) = ( lim_sup seq)

    proof

      let seq be ExtREAL_sequence;

      assume that

       A1: ( lim_inf seq) = ( lim_sup seq) and

       A2: ( lim_inf seq) in REAL ;

      consider k be Nat such that

       A3: (seq ^\ k) is bounded by A1, A2, Th18;

      reconsider rseq0 = (seq ^\ k) as Real_Sequence by A3, Th11;

      (seq ^\ k) is bounded_below by A3;

      then

       A4: rseq0 is bounded_below by Th13;

      

       A5: k in NAT by ORDINAL1:def 12;

      (seq ^\ k) is bounded_above by A3;

      then

       A6: rseq0 is bounded_above by Th12;

      then ( lim_sup rseq0) = ( lim_sup (seq ^\ k)) by A4, Th9;

      then

       A7: ( lim_sup rseq0) = ( lim_sup seq) by Th28, A5;

      ( lim_inf rseq0) = ( lim_inf (seq ^\ k)) by A6, A4, Th10;

      then

       A8: ( lim_inf rseq0) = ( lim_inf seq) by Th29, A5;

      then

       A9: rseq0 is convergent by A1, A6, A4, A7, RINFSUP1: 88;

      then

       A10: ( lim rseq0) = ( lim_inf seq) by A8, RINFSUP1: 89;

      

       A11: (seq ^\ k) is convergent by A9, Th14;

      

       A12: ( lim rseq0) = ( lim (seq ^\ k)) by A9, Th14;

      ( lim rseq0) = ( lim_sup seq) by A7, A9, RINFSUP1: 89;

      hence thesis by A10, A12, A11, Th17;

    end;

    theorem :: RINFSUP2:40

    

     Th40: for seq be ExtREAL_sequence holds seq is convergent iff ( lim_inf seq) = ( lim_sup seq)

    proof

      let seq be ExtREAL_sequence;

      set a = ( lim_inf seq);

      thus seq is convergent implies ( lim_inf seq) = ( lim_sup seq)

      proof

        assume

         A1: seq is convergent;

        per cases by A1, MESFUNC5:def 11;

          suppose

           A2: seq is convergent_to_finite_number;

          then

          consider k be Nat such that

           A3: (seq ^\ k) is bounded by Th19;

          reconsider rseq0 = (seq ^\ k) as Real_Sequence by A3, Th11;

          

           A4: k in NAT by ORDINAL1:def 12;

          (seq ^\ k) is convergent_to_finite_number by A2, Th20;

          then

           A5: rseq0 is convergent by Th15;

          then

           A6: rseq0 is bounded;

          then ( lim_sup rseq0) = ( lim_sup (seq ^\ k)) by Th9;

          then

           A7: ( lim_sup rseq0) = ( lim_sup seq) by Th28, A4;

          ( lim_inf rseq0) = ( lim_inf (seq ^\ k)) by A6, Th10;

          then ( lim_inf rseq0) = ( lim_inf seq) by Th29, A4;

          hence thesis by A5, A7, RINFSUP1: 88;

        end;

          suppose

           A8: seq is convergent_to_-infty;

          now

            let g be Real;

            assume g < 0 ;

            then

            consider n be Nat such that

             A9: for m be Nat st n <= m holds (seq . m) <= g by A8, MESFUNC5:def 10;

            now

              let m be Nat;

              

               A10: (( inferior_realsequence seq) . m) <= (seq . m) by Th8;

              assume n <= m;

              then (seq . m) <= g by A9;

              hence (( inferior_realsequence seq) . m) <= g by A10, XXREAL_0: 2;

            end;

            hence ex n be Nat st for m be Nat st n <= m holds (( inferior_realsequence seq) . m) <= g;

          end;

          then

           A11: ( inferior_realsequence seq) is convergent_to_-infty by MESFUNC5:def 10;

          then ( inferior_realsequence seq) is convergent by MESFUNC5:def 11;

          then ( lim ( inferior_realsequence seq)) = -infty by A11, MESFUNC5:def 12;

          then

           A12: ( lim_inf seq) = -infty by Th37;

          

           A13: ( superior_realsequence seq) is convergent_to_-infty

          proof

            set iseq = ( superior_realsequence seq);

            assume not iseq is convergent_to_-infty;

            then

            consider g be Real such that

             A14: g < 0 and

             A15: for n be Nat holds ex m be Nat st n <= m & g < (iseq . m) by MESFUNC5:def 10;

            consider N be Nat such that

             A16: for m be Nat st N <= m holds (seq . m) <= g by A8, A14, MESFUNC5:def 10;

            now

              let m be Nat;

              consider Y be non empty Subset of ExtREAL such that

               A17: Y = { (seq . k) : m <= k } and

               A18: (( superior_realsequence seq) . m) = ( sup Y) by Def7;

              assume

               A19: N <= m;

              now

                let x be ExtReal;

                assume x in Y;

                then

                consider k be Nat such that

                 A20: x = (seq . k) and

                 A21: m <= k by A17;

                N <= k by A19, A21, XXREAL_0: 2;

                hence x <= g by A16, A20;

              end;

              then g is UpperBound of Y by XXREAL_2:def 1;

              hence (iseq . m) <= g by A18, XXREAL_2:def 3;

            end;

            hence contradiction by A15;

          end;

          then ( superior_realsequence seq) is convergent by MESFUNC5:def 11;

          then ( lim ( superior_realsequence seq)) = -infty by A13, MESFUNC5:def 12;

          hence thesis by A12, Th36;

        end;

          suppose

           A22: seq is convergent_to_+infty;

          now

            let g be Real;

            assume 0 < g;

            then

            consider n be Nat such that

             A23: for m be Nat st n <= m holds g <= (seq . m) by A22, MESFUNC5:def 9;

            now

              let m be Nat;

              

               A24: (seq . m) <= (( superior_realsequence seq) . m) by Th8;

              assume n <= m;

              then g <= (seq . m) by A23;

              hence g <= (( superior_realsequence seq) . m) by A24, XXREAL_0: 2;

            end;

            hence ex n be Nat st for m be Nat st n <= m holds g <= (( superior_realsequence seq) . m);

          end;

          then

           A25: ( superior_realsequence seq) is convergent_to_+infty by MESFUNC5:def 9;

          then ( superior_realsequence seq) is convergent by MESFUNC5:def 11;

          then ( lim ( superior_realsequence seq)) = +infty by A25, MESFUNC5:def 12;

          then

           A26: ( lim_sup seq) = +infty by Th36;

          

           A27: ( inferior_realsequence seq) is convergent_to_+infty

          proof

            set iseq = ( inferior_realsequence seq);

            assume not iseq is convergent_to_+infty;

            then

            consider g be Real such that

             A28: 0 < g and

             A29: for n be Nat holds ex m be Nat st n <= m & (iseq . m) < g by MESFUNC5:def 9;

            consider N be Nat such that

             A30: for m be Nat st N <= m holds g <= (seq . m) by A22, A28, MESFUNC5:def 9;

            now

              let m be Nat;

              consider Y be non empty Subset of ExtREAL such that

               A31: Y = { (seq . k) : m <= k } and

               A32: (( inferior_realsequence seq) . m) = ( inf Y) by Def6;

              assume

               A33: N <= m;

              now

                let x be ExtReal;

                assume x in Y;

                then

                consider k be Nat such that

                 A34: x = (seq . k) and

                 A35: m <= k by A31;

                N <= k by A33, A35, XXREAL_0: 2;

                hence g <= x by A30, A34;

              end;

              then g is LowerBound of Y by XXREAL_2:def 2;

              hence g <= (iseq . m) by A32, XXREAL_2:def 4;

            end;

            hence contradiction by A29;

          end;

          then ( inferior_realsequence seq) is convergent by MESFUNC5:def 11;

          then ( lim ( inferior_realsequence seq)) = +infty by A27, MESFUNC5:def 12;

          hence thesis by A26, Th37;

        end;

      end;

      assume

       A36: ( lim_inf seq) = ( lim_sup seq);

      per cases by XXREAL_0: 14;

        suppose a in REAL ;

        hence thesis by A36, Lm7;

      end;

        suppose a = +infty ;

        hence thesis by A36, Lm5;

      end;

        suppose a = -infty ;

        hence thesis by A36, Lm6;

      end;

    end;

    theorem :: RINFSUP2:41

    for seq be ExtREAL_sequence st seq is convergent holds ( lim seq) = ( lim_inf seq) & ( lim seq) = ( lim_sup seq)

    proof

      let seq be ExtREAL_sequence;

      set a = ( lim_inf seq);

      assume seq is convergent;

      then

       A1: ( lim_inf seq) = ( lim_sup seq) by Th40;

      per cases by XXREAL_0: 14;

        suppose a in REAL ;

        hence thesis by A1, Lm7;

      end;

        suppose a = +infty ;

        hence thesis by A1, Lm5;

      end;

        suppose a = -infty ;

        hence thesis by A1, Lm6;

      end;

    end;