limfunc1.miz



    begin

    reserve r,r1,g for Real,

n,m,k for Nat,

seq,seq1,seq2 for Real_Sequence,

f,f1,f2 for PartFunc of REAL , REAL ,

x for set;

    

     Lm1: 0 < g & r <= r1 implies (r - g) < r1 & r < (r1 + g)

    proof

      assume

       A1: 0 < g & r <= r1;

      then (r - g) < (r1 - 0 ) by XREAL_1: 15;

      hence (r - g) < r1;

      (r + 0 ) < (r1 + g) by A1, XREAL_1: 8;

      hence thesis;

    end;

    

     Lm2: ( rng seq) c= ( dom (f1 + f2)) implies ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) & ( rng seq) c= ( dom f1) & ( rng seq) c= ( dom f2)

    proof

      assume

       A1: ( rng seq) c= ( dom (f1 + f2));

      thus ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by VALUED_1:def 1;

      then ( dom (f1 + f2)) c= ( dom f1) & ( dom (f1 + f2)) c= ( dom f2) by XBOOLE_1: 17;

      hence thesis by A1;

    end;

    

     Lm3: ( rng seq) c= ( dom (f1 (#) f2)) implies ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) & ( rng seq) c= ( dom f1) & ( rng seq) c= ( dom f2)

    proof

      assume

       A1: ( rng seq) c= ( dom (f1 (#) f2));

      thus ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

      then ( dom (f1 (#) f2)) c= ( dom f1) & ( dom (f1 (#) f2)) c= ( dom f2) by XBOOLE_1: 17;

      hence thesis by A1;

    end;

    notation

      let r be Real;

      synonym left_open_halfline r for halfline r;

    end

    definition

      let r be Real;

      :: LIMFUNC1:def1

      func left_closed_halfline r -> Subset of REAL equals ]. -infty , r.];

      coherence

      proof

        for x be object st x in ]. -infty , r.] holds x in REAL by XREAL_0:def 1;

        hence thesis by TARSKI:def 3;

      end;

      :: LIMFUNC1:def2

      func right_closed_halfline r -> Subset of REAL equals [.r, +infty .[;

      coherence

      proof

        for x be object st x in [.r, +infty .[ holds x in REAL by XREAL_0:def 1;

        hence thesis by TARSKI:def 3;

      end;

      :: LIMFUNC1:def3

      func right_open_halfline r -> Subset of REAL equals ].r, +infty .[;

      coherence

      proof

        for x be object st x in ].r, +infty .[ holds x in REAL by XREAL_0:def 1;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: LIMFUNC1:1

    (seq is non-decreasing implies seq is bounded_below) & (seq is non-increasing implies seq is bounded_above)

    proof

      thus seq is non-decreasing implies seq is bounded_below

      proof

        assume

         A1: seq is non-decreasing;

        take ((seq . 0 ) - 1);

        let n;

        ((seq . 0 ) - 1) < ((seq . 0 ) - 0 ) & (seq . 0 ) <= (seq . n) by A1, SEQM_3: 11, XREAL_1: 15;

        hence thesis by XXREAL_0: 2;

      end;

      assume

       A2: seq is non-increasing;

      take ((seq . 0 ) + 1);

      let n;

      ((seq . 0 ) + 0 ) < ((seq . 0 ) + 1) & (seq . n) <= (seq . 0 ) by A2, SEQM_3: 12, XREAL_1: 8;

      hence thesis by XXREAL_0: 2;

    end;

    theorem :: LIMFUNC1:2

    

     Th2: seq is non-zero & seq is convergent & ( lim seq) = 0 & seq is non-decreasing implies for n holds (seq . n) < 0

    proof

      assume that

       A1: seq is non-zero and

       A2: seq is convergent & ( lim seq) = 0 and

       A3: seq is non-decreasing and

       A4: ex n st not (seq . n) < 0 ;

      consider n such that

       A5: not (seq . n) < 0 by A4;

      now

        per cases by A5;

          suppose

           A6: 0 < (seq . n);

          then

          consider n1 be Nat such that

           A7: for m st n1 <= m holds |.((seq . m) - 0 ).| < (seq . n) by A2, SEQ_2:def 7;

           |.((seq . (n1 + n)) - 0 ).| < (seq . n) by A7, NAT_1: 12;

          then n <= (n1 + n) & (seq . (n1 + n)) < (seq . n) by A6, ABSVALUE:def 1, NAT_1: 12;

          hence contradiction by A3, SEQM_3: 6;

        end;

          suppose (seq . n) = 0 ;

          hence contradiction by A1, SEQ_1: 5;

        end;

      end;

      hence contradiction;

    end;

    theorem :: LIMFUNC1:3

    

     Th3: seq is non-zero & seq is convergent & ( lim seq) = 0 & seq is non-increasing implies for n holds 0 < (seq . n)

    proof

      assume that

       A1: seq is non-zero and

       A2: seq is convergent & ( lim seq) = 0 and

       A3: seq is non-increasing and

       A4: ex n st not 0 < (seq . n);

      consider n such that

       A5: not 0 < (seq . n) by A4;

      now

        per cases by A5;

          suppose

           A6: (seq . n) < 0 ;

          then ( - 0 ) < ( - (seq . n)) by XREAL_1: 24;

          then

          consider n1 be Nat such that

           A7: for m st n1 <= m holds |.((seq . m) - 0 ).| < ( - (seq . n)) by A2, SEQ_2:def 7;

          

           A8: |.((seq . (n1 + n)) - 0 ).| < ( - (seq . n)) by A7, NAT_1: 12;

          

           A9: n <= (n1 + n) by NAT_1: 12;

          then (seq . (n1 + n)) < 0 by A3, A6, SEQM_3: 8;

          then ( - (seq . (n1 + n))) < ( - (seq . n)) by A8, ABSVALUE:def 1;

          then (seq . n) < (seq . (n1 + n)) by XREAL_1: 24;

          hence contradiction by A3, A9, SEQM_3: 8;

        end;

          suppose (seq . n) = 0 ;

          hence contradiction by A1, SEQ_1: 5;

        end;

      end;

      hence contradiction;

    end;

    theorem :: LIMFUNC1:4

    

     Th4: seq is convergent & 0 < ( lim seq) implies ex n st for m st n <= m holds 0 < (seq . m)

    proof

      assume that

       A1: seq is convergent and

       A2: 0 < ( lim seq) and

       A3: for n holds ex m st n <= m & not 0 < (seq . m);

      consider n such that

       A4: for m st n <= m holds |.((seq . m) - ( lim seq)).| < ( lim seq) by A1, A2, SEQ_2:def 7;

      consider m such that

       A5: n <= m and

       A6: not 0 < (seq . m) by A3;

      

       A7: |.((seq . m) - ( lim seq)).| < ( lim seq) by A4, A5;

      now

        per cases by A6;

          suppose

           A8: (seq . m) < 0 ;

          then ( - ((seq . m) - ( lim seq))) < ( lim seq) by A2, A7, ABSVALUE:def 1;

          then (( lim seq) - (seq . m)) < ( lim seq);

          then ( lim seq) < (( lim seq) + (seq . m)) by XREAL_1: 19;

          then (( lim seq) - ( lim seq)) < (seq . m) by XREAL_1: 19;

          hence contradiction by A8;

        end;

          suppose (seq . m) = 0 ;

          then |.( - ( lim seq)).| < ( lim seq) by A7;

          then |.( lim seq).| < ( lim seq) by COMPLEX1: 52;

          hence contradiction by A2, ABSVALUE:def 1;

        end;

      end;

      hence contradiction;

    end;

    theorem :: LIMFUNC1:5

    

     Th5: seq is convergent & 0 < ( lim seq) implies ex n st for m st n <= m holds (( lim seq) / 2) < (seq . m)

    proof

      assume that

       A1: seq is convergent and

       A2: 0 < ( lim seq);

      reconsider ls = (( lim seq) / 2) as Element of REAL by XREAL_0:def 1;

      set s1 = ( seq_const (( lim seq) / 2));

      

       A3: (seq - s1) is convergent by A1;

      (s1 . 0 ) = (( lim seq) / 2) by SEQ_1: 57;

      

      then ( lim (seq - s1)) = (((( lim seq) / 2) + (( lim seq) / 2)) - (( lim seq) / 2)) by A1, SEQ_4: 42

      .= (( lim seq) / 2);

      then

      consider n such that

       A4: for m st n <= m holds 0 < ((seq - s1) . m) by A2, A3, Th4, XREAL_1: 215;

      take n;

      let m;

      assume n <= m;

      then 0 < ((seq - s1) . m) by A4;

      then 0 < ((seq . m) - (s1 . m)) by RFUNCT_2: 1;

      then 0 < ((seq . m) - (( lim seq) / 2)) by SEQ_1: 57;

      then ( 0 + (( lim seq) / 2)) < (seq . m) by XREAL_1: 20;

      hence thesis;

    end;

    reserve r,r1,r2,g,g1,g2 for Real;

    definition

      let seq;

      :: LIMFUNC1:def4

      attr seq is divergent_to+infty means for r holds ex n st for m st n <= m holds r < (seq . m);

      :: LIMFUNC1:def5

      attr seq is divergent_to-infty means for r holds ex n st for m st n <= m holds (seq . m) < r;

    end

    theorem :: LIMFUNC1:6

    seq is divergent_to+infty or seq is divergent_to-infty implies ex n st for m st n <= m holds (seq ^\ m) is non-zero

    proof

      assume

       A1: seq is divergent_to+infty or seq is divergent_to-infty;

      now

        per cases by A1;

          suppose seq is divergent_to+infty;

          then

          consider n such that

           A2: for m st n <= m holds 0 < (seq . m);

          take n;

          let m such that

           A3: n <= m;

          now

            let k;

             0 < (seq . (k + m)) by A2, A3, NAT_1: 12;

            hence 0 <> ((seq ^\ m) . k) by NAT_1:def 3;

          end;

          hence (seq ^\ m) is non-zero by SEQ_1: 5;

        end;

          suppose seq is divergent_to-infty;

          then

          consider n such that

           A4: for m st n <= m holds (seq . m) < 0 ;

          take n;

          let m such that

           A5: n <= m;

          now

            let k;

            (seq . (k + m)) < 0 by A4, A5, NAT_1: 12;

            hence ((seq ^\ m) . k) <> 0 by NAT_1:def 3;

          end;

          hence (seq ^\ m) is non-zero by SEQ_1: 5;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC1:7

    

     Th7: ((seq ^\ k) is divergent_to+infty implies seq is divergent_to+infty) & ((seq ^\ k) is divergent_to-infty implies seq is divergent_to-infty)

    proof

      thus (seq ^\ k) is divergent_to+infty implies seq is divergent_to+infty

      proof

        assume

         A1: (seq ^\ k) is divergent_to+infty;

        let r;

        consider n1 be Nat such that

         A2: for m st n1 <= m holds r < ((seq ^\ k) . m) by A1;

        take n = (n1 + k);

        let m;

        assume n <= m;

        then

        consider n2 be Nat such that

         A3: m = (n + n2) by NAT_1: 10;

        reconsider n2 as Element of NAT by ORDINAL1:def 12;

        

         A4: r < ((seq ^\ k) . (n1 + n2)) by A2, NAT_1: 12;

        ((n1 + n2) + k) = m by A3;

        hence thesis by A4, NAT_1:def 3;

      end;

      assume

       A5: (seq ^\ k) is divergent_to-infty;

      let r;

      consider n1 be Nat such that

       A6: for m st n1 <= m holds ((seq ^\ k) . m) < r by A5;

      take n = (n1 + k);

      let m;

      assume n <= m;

      then

      consider n2 be Nat such that

       A7: m = (n + n2) by NAT_1: 10;

      reconsider n2 as Element of NAT by ORDINAL1:def 12;

      

       A8: ((seq ^\ k) . (n1 + n2)) < r by A6, NAT_1: 12;

      ((n1 + n2) + k) = m by A7;

      hence thesis by A8, NAT_1:def 3;

    end;

    theorem :: LIMFUNC1:8

    

     Th8: seq1 is divergent_to+infty & seq2 is divergent_to+infty implies (seq1 + seq2) is divergent_to+infty

    proof

      assume that

       A1: seq1 is divergent_to+infty and

       A2: seq2 is divergent_to+infty;

      let r;

      consider n1 be Nat such that

       A3: for m st n1 <= m holds (r / 2) < (seq1 . m) by A1;

      consider n2 be Nat such that

       A4: for m st n2 <= m holds (r / 2) < (seq2 . m) by A2;

      reconsider n = ( max (n1,n2)) as Nat by TARSKI: 1;

      take n;

      let m such that

       A5: n <= m;

      n2 <= n by XXREAL_0: 25;

      then n2 <= m by A5, XXREAL_0: 2;

      then

       A6: (r / 2) < (seq2 . m) by A4;

      n1 <= n by XXREAL_0: 25;

      then n1 <= m by A5, XXREAL_0: 2;

      then (r / 2) < (seq1 . m) by A3;

      then ((r / 2) + (r / 2)) < ((seq1 . m) + (seq2 . m)) by A6, XREAL_1: 8;

      hence thesis by SEQ_1: 7;

    end;

    theorem :: LIMFUNC1:9

    

     Th9: seq1 is divergent_to+infty & seq2 is bounded_below implies (seq1 + seq2) is divergent_to+infty

    proof

      assume that

       A1: seq1 is divergent_to+infty and

       A2: seq2 is bounded_below;

      let r;

      consider M be Real such that

       A3: for n holds M < (seq2 . n) by A2;

      consider n such that

       A4: for m st n <= m holds (r - M) < (seq1 . m) by A1;

      take n;

      let m;

      assume n <= m;

      then (r - M) < (seq1 . m) by A4;

      then ((r - M) + M) < ((seq1 . m) + (seq2 . m)) by A3, XREAL_1: 8;

      hence thesis by SEQ_1: 7;

    end;

    theorem :: LIMFUNC1:10

    

     Th10: seq1 is divergent_to+infty & seq2 is divergent_to+infty implies (seq1 (#) seq2) is divergent_to+infty

    proof

      assume that

       A1: seq1 is divergent_to+infty and

       A2: seq2 is divergent_to+infty;

      let r;

      consider n1 be Nat such that

       A3: for m st n1 <= m holds ( sqrt |.r.|) < (seq1 . m) by A1;

      consider n2 be Nat such that

       A4: for m st n2 <= m holds ( sqrt |.r.|) < (seq2 . m) by A2;

      reconsider n = ( max (n1,n2)) as Nat by TARSKI: 1;

      take n;

      let m such that

       A5: n <= m;

      n2 <= n by XXREAL_0: 25;

      then n2 <= m by A5, XXREAL_0: 2;

      then

       A6: ( sqrt |.r.|) < (seq2 . m) by A4;

      n1 <= n by XXREAL_0: 25;

      then n1 <= m by A5, XXREAL_0: 2;

      then

       A7: ( sqrt |.r.|) < (seq1 . m) by A3;

      

       A8: |.r.| >= 0 by COMPLEX1: 46;

      then ( sqrt |.r.|) >= 0 by SQUARE_1:def 2;

      then (( sqrt |.r.|) ^2 ) < ((seq1 . m) * (seq2 . m)) by A7, A6, XREAL_1: 96;

      then

       A9: |.r.| < ((seq1 . m) * (seq2 . m)) by A8, SQUARE_1:def 2;

      r <= |.r.| by ABSVALUE: 4;

      then r < ((seq1 . m) * (seq2 . m)) by A9, XXREAL_0: 2;

      hence thesis by SEQ_1: 8;

    end;

    theorem :: LIMFUNC1:11

    

     Th11: seq1 is divergent_to-infty & seq2 is divergent_to-infty implies (seq1 + seq2) is divergent_to-infty

    proof

      assume that

       A1: seq1 is divergent_to-infty and

       A2: seq2 is divergent_to-infty;

      let r;

      consider n1 be Nat such that

       A3: for m st n1 <= m holds (seq1 . m) < (r / 2) by A1;

      consider n2 be Nat such that

       A4: for m st n2 <= m holds (seq2 . m) < (r / 2) by A2;

      reconsider n = ( max (n1,n2)) as Nat by TARSKI: 1;

      take n;

      let m such that

       A5: n <= m;

      n2 <= n by XXREAL_0: 25;

      then n2 <= m by A5, XXREAL_0: 2;

      then

       A6: (seq2 . m) < (r / 2) by A4;

      n1 <= n by XXREAL_0: 25;

      then n1 <= m by A5, XXREAL_0: 2;

      then (seq1 . m) < (r / 2) by A3;

      then ((seq1 . m) + (seq2 . m)) < ((r / 2) + (r / 2)) by A6, XREAL_1: 8;

      hence thesis by SEQ_1: 7;

    end;

    theorem :: LIMFUNC1:12

    

     Th12: seq1 is divergent_to-infty & seq2 is bounded_above implies (seq1 + seq2) is divergent_to-infty

    proof

      assume that

       A1: seq1 is divergent_to-infty and

       A2: seq2 is bounded_above;

      let r;

      consider M be Real such that

       A3: for n holds (seq2 . n) < M by A2;

      consider n such that

       A4: for m st n <= m holds (seq1 . m) < (r - M) by A1;

      take n;

      let m;

      assume n <= m;

      then (seq1 . m) < (r - M) by A4;

      then ((seq1 . m) + (seq2 . m)) < ((r - M) + M) by A3, XREAL_1: 8;

      hence thesis by SEQ_1: 7;

    end;

    

     Lm4: 0 in REAL by XREAL_0:def 1;

    theorem :: LIMFUNC1:13

    

     Th13: (seq is divergent_to+infty & r > 0 implies (r (#) seq) is divergent_to+infty) & (seq is divergent_to+infty & r < 0 implies (r (#) seq) is divergent_to-infty) & (r = 0 implies ( rng (r (#) seq)) = { 0 } & (r (#) seq) is constant)

    proof

      thus seq is divergent_to+infty & r > 0 implies (r (#) seq) is divergent_to+infty

      proof

        assume that

         A1: seq is divergent_to+infty and

         A2: r > 0 ;

        let g;

        consider n such that

         A3: for m st n <= m holds (g / r) < (seq . m) by A1;

        take n;

        let m;

        assume n <= m;

        then (g / r) < (seq . m) by A3;

        then ((g / r) * r) < (r * (seq . m)) by A2, XREAL_1: 68;

        then g < (r * (seq . m)) by A2, XCMPLX_1: 87;

        hence thesis by SEQ_1: 9;

      end;

      thus seq is divergent_to+infty & r < 0 implies (r (#) seq) is divergent_to-infty

      proof

        assume that

         A4: seq is divergent_to+infty and

         A5: r < 0 ;

        let g;

        consider n such that

         A6: for m st n <= m holds (g / r) < (seq . m) by A4;

        take n;

        let m;

        assume n <= m;

        then (g / r) < (seq . m) by A6;

        then (r * (seq . m)) < ((g / r) * r) by A5, XREAL_1: 69;

        then (r * (seq . m)) < g by A5, XCMPLX_1: 87;

        hence thesis by SEQ_1: 9;

      end;

      assume

       A7: r = 0 ;

      thus ( rng (r (#) seq)) = { 0 }

      proof

        let x be Real;

        thus x in ( rng (r (#) seq)) implies x in { 0 }

        proof

          assume x in ( rng (r (#) seq));

          then

          consider n be Element of NAT such that

           A8: x = ((r (#) seq) . n) by FUNCT_2: 113;

          x = (r * (seq . n)) by A8, SEQ_1: 9

          .= 0 by A7;

          hence thesis by TARSKI:def 1;

        end;

        assume x in { 0 };

        then

         A9: x = 0 by TARSKI:def 1;

        ((r (#) seq) . 0 ) = (r * (seq . 0 )) by SEQ_1: 9

        .= 0 by A7;

        hence thesis by A9, VALUED_0: 28;

      end;

      hence thesis by FUNCT_2: 111, Lm4;

    end;

    theorem :: LIMFUNC1:14

    

     Th14: (seq is divergent_to-infty & r > 0 implies (r (#) seq) is divergent_to-infty) & (seq is divergent_to-infty & r < 0 implies (r (#) seq) is divergent_to+infty) & (r = 0 implies ( rng (r (#) seq)) = { 0 } & (r (#) seq) is constant)

    proof

      thus seq is divergent_to-infty & r > 0 implies (r (#) seq) is divergent_to-infty

      proof

        assume that

         A1: seq is divergent_to-infty and

         A2: r > 0 ;

        let g;

        consider n such that

         A3: for m st n <= m holds (seq . m) < (g / r) by A1;

        take n;

        let m;

        assume n <= m;

        then (seq . m) < (g / r) by A3;

        then (r * (seq . m)) < ((g / r) * r) by A2, XREAL_1: 68;

        then (r * (seq . m)) < g by A2, XCMPLX_1: 87;

        hence thesis by SEQ_1: 9;

      end;

      thus seq is divergent_to-infty & r < 0 implies (r (#) seq) is divergent_to+infty

      proof

        assume that

         A4: seq is divergent_to-infty and

         A5: r < 0 ;

        let g;

        consider n such that

         A6: for m st n <= m holds (seq . m) < (g / r) by A4;

        take n;

        let m;

        assume n <= m;

        then (seq . m) < (g / r) by A6;

        then ((g / r) * r) < (r * (seq . m)) by A5, XREAL_1: 69;

        then g < (r * (seq . m)) by A5, XCMPLX_1: 87;

        hence thesis by SEQ_1: 9;

      end;

      assume

       A7: r = 0 ;

      thus ( rng (r (#) seq)) = { 0 }

      proof

        let x be Real;

        thus x in ( rng (r (#) seq)) implies x in { 0 }

        proof

          assume x in ( rng (r (#) seq));

          then

          consider n be Element of NAT such that

           A8: x = ((r (#) seq) . n) by FUNCT_2: 113;

          x = (r * (seq . n)) by A8, SEQ_1: 9

          .= 0 by A7;

          hence thesis by TARSKI:def 1;

        end;

        assume x in { 0 };

        then

         A9: x = 0 by TARSKI:def 1;

        ((r (#) seq) . 0 ) = (r * (seq . 0 )) by SEQ_1: 9

        .= 0 by A7;

        hence thesis by A9, VALUED_0: 28;

      end;

      hence thesis by FUNCT_2: 111, Lm4;

    end;

    reconsider jj = 1 as Real;

    theorem :: LIMFUNC1:15

    (seq is divergent_to+infty implies ( - seq) is divergent_to-infty) & (seq is divergent_to-infty implies ( - seq) is divergent_to+infty) by Th13, Th14;

    theorem :: LIMFUNC1:16

    seq is bounded_below & seq1 is divergent_to-infty implies (seq - seq1) is divergent_to+infty

    proof

      assume that

       A1: seq is bounded_below and

       A2: seq1 is divergent_to-infty;

      (( - jj) (#) seq1) is divergent_to+infty by A2, Th14;

      hence thesis by A1, Th9;

    end;

    theorem :: LIMFUNC1:17

    seq is bounded_above & seq1 is divergent_to+infty implies (seq - seq1) is divergent_to-infty

    proof

      assume that

       A1: seq is bounded_above and

       A2: seq1 is divergent_to+infty;

      (( - jj) (#) seq1) is divergent_to-infty by A2, Th13;

      hence thesis by A1, Th12;

    end;

    theorem :: LIMFUNC1:18

    seq is divergent_to+infty & seq1 is convergent implies (seq + seq1) is divergent_to+infty by Th9;

    theorem :: LIMFUNC1:19

    seq is divergent_to-infty & seq1 is convergent implies (seq + seq1) is divergent_to-infty by Th12;

    theorem :: LIMFUNC1:20

    

     Th20: (for n holds (seq . n) = n) implies seq is divergent_to+infty

    proof

      assume

       A1: for n holds (seq . n) = n;

      let r;

      consider n such that

       A2: r < n by SEQ_4: 3;

      take n;

      let m;

      assume n <= m;

      then r < m by A2, XXREAL_0: 2;

      hence thesis by A1;

    end;

    reconsider s1 = ( id NAT ) as Real_Sequence by FUNCT_2: 7, NUMBERS: 19;

    

     Lm5: for n holds (s1 . n) = n by ORDINAL1:def 12, FUNCT_1: 18;

    theorem :: LIMFUNC1:21

    

     Th21: (for n holds (seq . n) = ( - n)) implies seq is divergent_to-infty

    proof

      assume

       A1: for n holds (seq . n) = ( - n);

       A2:

      now

        let n be Element of NAT ;

        

        thus (( - s1) . n) = ( - (s1 . n)) by SEQ_1: 10

        .= ( - n)

        .= (seq . n) by A1;

      end;

      s1 is divergent_to+infty by Lm5, Th20;

      then (( - jj) (#) s1) is divergent_to-infty by Th13;

      hence thesis by A2, FUNCT_2: 63;

    end;

    theorem :: LIMFUNC1:22

    

     Th22: seq1 is divergent_to+infty & (ex r st r > 0 & for n holds (seq2 . n) >= r) implies (seq1 (#) seq2) is divergent_to+infty

    proof

      assume that

       A1: seq1 is divergent_to+infty and

       A2: ex r st r > 0 & for n holds (seq2 . n) >= r;

      consider M be Real such that

       A3: M > 0 and

       A4: for n holds (seq2 . n) >= M by A2;

      let r;

      

       A5: 0 <= |.r.| by COMPLEX1: 46;

      consider n such that

       A6: for m st n <= m holds ( |.r.| / M) < (seq1 . m) by A1;

      take n;

      let m;

      assume n <= m;

      then ( |.r.| / M) < (seq1 . m) by A6;

      then (( |.r.| / M) * M) < ((seq1 . m) * (seq2 . m)) by A3, A4, A5, XREAL_1: 97;

      then

       A7: |.r.| < ((seq1 . m) * (seq2 . m)) by A3, XCMPLX_1: 87;

      r <= |.r.| by ABSVALUE: 4;

      then r < ((seq1 . m) * (seq2 . m)) by A7, XXREAL_0: 2;

      hence thesis by SEQ_1: 8;

    end;

    theorem :: LIMFUNC1:23

    seq1 is divergent_to-infty & (ex r st 0 < r & for n holds (seq2 . n) >= r) implies (seq1 (#) seq2) is divergent_to-infty

    proof

      assume that

       A1: seq1 is divergent_to-infty and

       A2: ex r st 0 < r & for n holds (seq2 . n) >= r;

      (( - jj) (#) seq1) is divergent_to+infty by A1, Th14;

      then

       A3: ((( - jj) (#) seq1) (#) seq2) is divergent_to+infty by A2, Th22;

      (( - 1) (#) ((( - 1) (#) seq1) (#) seq2)) = (( - 1) (#) (( - 1) (#) (seq1 (#) seq2))) by SEQ_1: 18

      .= ((( - 1) * ( - 1)) (#) (seq1 (#) seq2)) by SEQ_1: 23

      .= (seq1 (#) seq2) by SEQ_1: 27;

      hence thesis by A3, Th13;

    end;

    theorem :: LIMFUNC1:24

    

     Th24: seq1 is divergent_to-infty & seq2 is divergent_to-infty implies (seq1 (#) seq2) is divergent_to+infty

    proof

      assume seq1 is divergent_to-infty & seq2 is divergent_to-infty;

      then

       A1: (( - jj) (#) seq1) is divergent_to+infty & (( - jj) (#) seq2) is divergent_to+infty by Th14;

      ((( - 1) (#) seq1) (#) (( - 1) (#) seq2)) = (( - 1) (#) (seq1 (#) (( - 1) (#) seq2))) by SEQ_1: 18

      .= (( - 1) (#) (( - 1) (#) (seq1 (#) seq2))) by SEQ_1: 19

      .= ((( - 1) * ( - 1)) (#) (seq1 (#) seq2)) by SEQ_1: 23

      .= (seq1 (#) seq2) by SEQ_1: 27;

      hence thesis by A1, Th10;

    end;

    theorem :: LIMFUNC1:25

    

     Th25: (seq is divergent_to+infty or seq is divergent_to-infty) implies ( abs seq) is divergent_to+infty

    proof

      assume

       A1: seq is divergent_to+infty or seq is divergent_to-infty;

      let r;

      now

        per cases by A1;

          suppose seq is divergent_to+infty;

          then

          consider n such that

           A2: for m st n <= m holds |.r.| < (seq . m);

          take n;

          let m;

          assume n <= m;

          then r <= |.r.| & |.r.| < (seq . m) by A2, ABSVALUE: 4;

          then

           A3: r < (seq . m) by XXREAL_0: 2;

          (seq . m) <= |.(seq . m).| by ABSVALUE: 4;

          then (seq . m) <= (( abs seq) . m) by SEQ_1: 12;

          hence r < (( abs seq) . m) by A3, XXREAL_0: 2;

        end;

          suppose seq is divergent_to-infty;

          then

          consider n such that

           A4: for m st n <= m holds (seq . m) < ( - r);

          take n;

          let m;

          ( - |.(seq . m).|) <= (seq . m) by ABSVALUE: 4;

          then

           A5: ( - (( abs seq) . m)) <= (seq . m) by SEQ_1: 12;

          assume n <= m;

          then (seq . m) < ( - r) by A4;

          then ( - (( abs seq) . m)) < ( - r) by A5, XXREAL_0: 2;

          hence r < (( abs seq) . m) by XREAL_1: 24;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC1:26

    

     Th26: seq is divergent_to+infty & seq1 is subsequence of seq implies seq1 is divergent_to+infty

    proof

      assume that

       A1: seq is divergent_to+infty and

       A2: seq1 is subsequence of seq;

      consider Ns be increasing sequence of NAT such that

       A3: seq1 = (seq * Ns) by A2, VALUED_0:def 17;

      let r;

      consider n such that

       A4: for m st n <= m holds r < (seq . m) by A1;

      take n;

      let m;

      assume

       A5: n <= m;

      

       A6: m in NAT by ORDINAL1:def 12;

      m <= (Ns . m) by SEQM_3: 14;

      then n <= (Ns . m) by A5, XXREAL_0: 2;

      then r < (seq . (Ns . m)) by A4;

      hence thesis by A3, FUNCT_2: 15, A6;

    end;

    theorem :: LIMFUNC1:27

    

     Th27: seq is divergent_to-infty & seq1 is subsequence of seq implies seq1 is divergent_to-infty

    proof

      assume that

       A1: seq is divergent_to-infty and

       A2: seq1 is subsequence of seq;

      consider Ns be increasing sequence of NAT such that

       A3: seq1 = (seq * Ns) by A2, VALUED_0:def 17;

      let r;

      consider n such that

       A4: for m st n <= m holds (seq . m) < r by A1;

      take n;

      let m;

      assume

       A5: n <= m;

      

       A6: m in NAT by ORDINAL1:def 12;

      m <= (Ns . m) by SEQM_3: 14;

      then n <= (Ns . m) by A5, XXREAL_0: 2;

      then (seq . (Ns . m)) < r by A4;

      hence thesis by A3, FUNCT_2: 15, A6;

    end;

    theorem :: LIMFUNC1:28

    seq1 is divergent_to+infty & seq2 is convergent & 0 < ( lim seq2) implies (seq1 (#) seq2) is divergent_to+infty

    proof

      assume that

       A1: seq1 is divergent_to+infty and

       A2: seq2 is convergent and

       A3: 0 < ( lim seq2);

      consider n1 be Nat such that

       A4: for m st n1 <= m holds (( lim seq2) / 2) < (seq2 . m) by A2, A3, Th5;

      now

        thus 0 < (( lim seq2) / 2) by A3, XREAL_1: 215;

        let n;

        (( lim seq2) / 2) < (seq2 . (n + n1)) by A4, NAT_1: 12;

        hence (( lim seq2) / 2) <= ((seq2 ^\ n1) . n) by NAT_1:def 3;

      end;

      then ((seq1 ^\ n1) (#) (seq2 ^\ n1)) is divergent_to+infty by A1, Th22, Th26;

      then ((seq1 (#) seq2) ^\ n1) is divergent_to+infty by SEQM_3: 19;

      hence thesis by Th7;

    end;

    theorem :: LIMFUNC1:29

    

     Th29: seq is non-decreasing & not seq is bounded_above implies seq is divergent_to+infty

    proof

      assume that

       A1: seq is non-decreasing and

       A2: not seq is bounded_above;

      let r;

      consider n such that

       A3: (r + 1) <= (seq . n) by A2;

      take n;

      let m;

      assume n <= m;

      then (seq . n) <= (seq . m) by A1, SEQM_3: 6;

      then (r + 1) <= (seq . m) by A3, XXREAL_0: 2;

      hence thesis by Lm1;

    end;

    theorem :: LIMFUNC1:30

    

     Th30: seq is non-increasing & not seq is bounded_below implies seq is divergent_to-infty

    proof

      assume that

       A1: seq is non-increasing and

       A2: not seq is bounded_below;

      let r;

      consider n such that

       A3: (seq . n) <= (r - 1) by A2;

      take n;

      let m;

      assume n <= m;

      then (seq . m) <= (seq . n) by A1, SEQM_3: 8;

      then (seq . m) <= (r - 1) by A3, XXREAL_0: 2;

      hence thesis by Lm1;

    end;

    theorem :: LIMFUNC1:31

    seq is increasing & not seq is bounded_above implies seq is divergent_to+infty by Th29;

    theorem :: LIMFUNC1:32

    seq is decreasing & not seq is bounded_below implies seq is divergent_to-infty by Th30;

    theorem :: LIMFUNC1:33

    seq is monotone implies seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty

    proof

      assume

       A1: seq is monotone;

      now

        per cases by A1, SEQM_3:def 5;

          suppose

           A2: seq is non-decreasing;

          now

            per cases ;

              suppose seq is bounded_above;

              hence thesis by A2;

            end;

              suppose not seq is bounded_above;

              hence thesis by A2, Th29;

            end;

          end;

          hence thesis;

        end;

          suppose

           A3: seq is non-increasing;

          now

            per cases ;

              suppose seq is bounded_below;

              hence thesis by A3;

            end;

              suppose not seq is bounded_below;

              hence thesis by A3, Th30;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC1:34

    

     Th34: (seq is divergent_to+infty or seq is divergent_to-infty) implies (seq " ) is convergent & ( lim (seq " )) = 0

    proof

      assume

       A1: seq is divergent_to+infty or seq is divergent_to-infty;

      now

        per cases by A1;

          suppose

           A2: seq is divergent_to+infty;

           A3:

          now

            let r be Real such that

             A4: 0 < r;

            consider n such that

             A5: for m st n <= m holds (r " ) < (seq . m) by A2;

            take n;

            let m;

            assume n <= m;

            then

             A6: (r " ) < (seq . m) by A5;

            then (1 / (seq . m)) < (1 / (r " )) by A4, XREAL_1: 76;

            then

             A7: (1 / (seq . m)) < r by XCMPLX_1: 216;

            

             A8: (1 / (seq . m)) = ((seq . m) " ) & ((seq . m) " ) = ((seq " ) . m) by VALUED_1: 10, XCMPLX_1: 215;

             0 < (r " ) by A4;

            hence |.(((seq " ) . m) - 0 ).| < r by A6, A7, A8, ABSVALUE:def 1;

          end;

          hence (seq " ) is convergent;

          hence thesis by A3, SEQ_2:def 7;

        end;

          suppose

           A9: seq is divergent_to-infty;

           A10:

          now

            let r be Real such that

             A11: 0 < r;

            

             A12: ( - (r " )) < ( - 0 ) by A11, XREAL_1: 24;

            consider n such that

             A13: for m st n <= m holds (seq . m) < ( - (r " )) by A9;

            take n;

            let m;

            assume

             A14: n <= m;

            then (seq . m) < ( - (r " )) by A13;

            then (1 / ( - (r " ))) < (1 / (seq . m)) by A12, XREAL_1: 99;

            then ((( - 1) * (r " )) " ) < (1 / (seq . m)) by XCMPLX_1: 215;

            then

             A15: ((( - 1) " ) * ((r " ) " )) < (1 / (seq . m)) by XCMPLX_1: 204;

            (seq . m) < ( - 0 ) by A11, A13, A14;

            then (1 / (seq . m)) < ( 0 / (seq . m)) by XREAL_1: 75;

            then |.(1 / (seq . m)).| = ( - (1 / (seq . m))) by ABSVALUE:def 1;

            then ( - (1 * r)) < ( - |.(1 / (seq . m)).|) by A15;

            then |.(1 / (seq . m)).| < r by XREAL_1: 24;

            then |.((seq . m) " ).| < r by XCMPLX_1: 215;

            hence |.(((seq " ) . m) - 0 ).| < r by VALUED_1: 10;

          end;

          hence (seq " ) is convergent;

          hence thesis by A10, SEQ_2:def 7;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC1:35

    

     Th35: seq is convergent & ( lim seq) = 0 & (ex k st for n st k <= n holds 0 < (seq . n)) implies (seq " ) is divergent_to+infty

    proof

      assume

       A1: seq is convergent & ( lim seq) = 0 ;

      given k such that

       A2: for n st k <= n holds 0 < (seq . n);

      let r;

      set l = ( |.r.| + 1);

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

      then

      consider o be Nat such that

       A3: for n st o <= n holds |.((seq . n) - 0 ).| < (l " ) by A1, SEQ_2:def 7;

      reconsider m = ( max (k,o)) as Nat by TARSKI: 1;

      take m;

      let n;

      assume

       A4: m <= n;

      k <= m by XXREAL_0: 25;

      then k <= n by A4, XXREAL_0: 2;

      then

       A5: 0 < (seq . n) by A2;

      o <= m by XXREAL_0: 25;

      then o <= n by A4, XXREAL_0: 2;

      then |.((seq . n) - 0 ).| < (l " ) by A3;

      then (seq . n) < (l " ) by A5, ABSVALUE:def 1;

      then (1 / (l " )) < (1 / (seq . n)) by A5, XREAL_1: 76;

      then

       A6: l < (1 / (seq . n)) by XCMPLX_1: 216;

      r <= |.r.| by ABSVALUE: 4;

      then r < l by Lm1;

      then r < (1 / (seq . n)) by A6, XXREAL_0: 2;

      then r < ((seq . n) " ) by XCMPLX_1: 215;

      hence thesis by VALUED_1: 10;

    end;

    theorem :: LIMFUNC1:36

    

     Th36: seq is convergent & ( lim seq) = 0 & (ex k st for n st k <= n holds (seq . n) < 0 ) implies (seq " ) is divergent_to-infty

    proof

      assume

       A1: seq is convergent & ( lim seq) = 0 ;

      given k such that

       A2: for n st k <= n holds (seq . n) < 0 ;

      let r;

      set l = ( |.r.| + 1);

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

      then

      consider o be Nat such that

       A3: for n st o <= n holds |.((seq . n) - 0 ).| < (l " ) by A1, SEQ_2:def 7;

      reconsider m = ( max (k,o)) as Nat by TARSKI: 1;

      take m;

      let n;

      assume

       A4: m <= n;

      k <= m by XXREAL_0: 25;

      then k <= n by A4, XXREAL_0: 2;

      then

       A5: (seq . n) < 0 by A2;

      then

       A6: 0 < ( - (seq . n)) by XREAL_1: 58;

      o <= m by XXREAL_0: 25;

      then o <= n by A4, XXREAL_0: 2;

      then |.((seq . n) - 0 ).| < (l " ) by A3;

      then ( - (seq . n)) < (l " ) by A5, ABSVALUE:def 1;

      then (1 / (l " )) < (1 / ( - (seq . n))) by A6, XREAL_1: 76;

      then l < (1 / ( - (seq . n))) by XCMPLX_1: 216;

      then l < (( - (seq . n)) " ) by XCMPLX_1: 215;

      then l < ( - ((seq . n) " )) by XCMPLX_1: 222;

      then

       A7: ( - ( - ((seq . n) " ))) < ( - l) by XREAL_1: 24;

      ( - |.r.|) <= r by ABSVALUE: 4;

      then (( - |.r.|) - 1) < r by Lm1;

      then ((seq . n) " ) < r by A7, XXREAL_0: 2;

      hence thesis by VALUED_1: 10;

    end;

    theorem :: LIMFUNC1:37

    

     Th37: seq is non-zero & seq is convergent & ( lim seq) = 0 & seq is non-decreasing implies (seq " ) is divergent_to-infty

    proof

      assume that

       A1: seq is non-zero and

       A2: seq is convergent & ( lim seq) = 0 and

       A3: seq is non-decreasing;

      for n holds 0 <= n implies (seq . n) < 0 by A1, A2, A3, Th2;

      hence thesis by A2, Th36;

    end;

    theorem :: LIMFUNC1:38

    

     Th38: seq is non-zero & seq is convergent & ( lim seq) = 0 & seq is non-increasing implies (seq " ) is divergent_to+infty

    proof

      assume that

       A1: seq is non-zero and

       A2: seq is convergent & ( lim seq) = 0 and

       A3: seq is non-increasing;

      for n holds 0 <= n implies 0 < (seq . n) by A1, A2, A3, Th3;

      hence thesis by A2, Th35;

    end;

    theorem :: LIMFUNC1:39

    seq is non-zero & seq is convergent & ( lim seq) = 0 & seq is increasing implies (seq " ) is divergent_to-infty by Th37;

    theorem :: LIMFUNC1:40

    seq is non-zero & seq is convergent & ( lim seq) = 0 & seq is decreasing implies (seq " ) is divergent_to+infty by Th38;

    theorem :: LIMFUNC1:41

    seq1 is bounded & (seq2 is divergent_to+infty or seq2 is divergent_to-infty) implies (seq1 /" seq2) is convergent & ( lim (seq1 /" seq2)) = 0

    proof

      assume that

       A1: seq1 is bounded and

       A2: seq2 is divergent_to+infty or seq2 is divergent_to-infty;

      (seq2 " ) is convergent & ( lim (seq2 " )) = 0 by A2, Th34;

      hence thesis by A1, SEQ_2: 25, SEQ_2: 26;

    end;

    theorem :: LIMFUNC1:42

    

     Th42: seq is divergent_to+infty & (for n holds (seq . n) <= (seq1 . n)) implies seq1 is divergent_to+infty

    proof

      assume that

       A1: seq is divergent_to+infty and

       A2: for n holds (seq . n) <= (seq1 . n);

      let r;

      consider n such that

       A3: for m st n <= m holds r < (seq . m) by A1;

      take n;

      let m;

      assume n <= m;

      then

       A4: r < (seq . m) by A3;

      (seq . m) <= (seq1 . m) by A2;

      hence thesis by A4, XXREAL_0: 2;

    end;

    theorem :: LIMFUNC1:43

    

     Th43: seq is divergent_to-infty & (for n holds (seq1 . n) <= (seq . n)) implies seq1 is divergent_to-infty

    proof

      assume that

       A1: seq is divergent_to-infty and

       A2: for n holds (seq1 . n) <= (seq . n);

      let r;

      consider n such that

       A3: for m st n <= m holds (seq . m) < r by A1;

      take n;

      let m;

      assume n <= m;

      then

       A4: (seq . m) < r by A3;

      (seq1 . m) <= (seq . m) by A2;

      hence thesis by A4, XXREAL_0: 2;

    end;

    definition

      let f;

      :: LIMFUNC1:def6

      attr f is convergent_in+infty means (for r holds ex g st r < g & g in ( dom f)) & ex g st for seq st seq is divergent_to+infty & ( rng seq) c= ( dom f) holds (f /* seq) is convergent & ( lim (f /* seq)) = g;

      :: LIMFUNC1:def7

      attr f is divergent_in+infty_to+infty means (for r holds ex g st r < g & g in ( dom f)) & for seq st seq is divergent_to+infty & ( rng seq) c= ( dom f) holds (f /* seq) is divergent_to+infty;

      :: LIMFUNC1:def8

      attr f is divergent_in+infty_to-infty means (for r holds ex g st r < g & g in ( dom f)) & for seq st seq is divergent_to+infty & ( rng seq) c= ( dom f) holds (f /* seq) is divergent_to-infty;

      :: LIMFUNC1:def9

      attr f is convergent_in-infty means (for r holds ex g st g < r & g in ( dom f)) & ex g st for seq st seq is divergent_to-infty & ( rng seq) c= ( dom f) holds (f /* seq) is convergent & ( lim (f /* seq)) = g;

      :: LIMFUNC1:def10

      attr f is divergent_in-infty_to+infty means (for r holds ex g st g < r & g in ( dom f)) & for seq st seq is divergent_to-infty & ( rng seq) c= ( dom f) holds (f /* seq) is divergent_to+infty;

      :: LIMFUNC1:def11

      attr f is divergent_in-infty_to-infty means (for r holds ex g st g < r & g in ( dom f)) & for seq st seq is divergent_to-infty & ( rng seq) c= ( dom f) holds (f /* seq) is divergent_to-infty;

    end

    theorem :: LIMFUNC1:44

    f is convergent_in+infty iff (for r holds ex g st r < g & g in ( dom f)) & ex g st for g1 st 0 < g1 holds ex r st for r1 st r < r1 & r1 in ( dom f) holds |.((f . r1) - g).| < g1

    proof

      thus f is convergent_in+infty implies (for r holds ex g st r < g & g in ( dom f)) & ex g st for g1 st 0 < g1 holds ex r st for r1 st r < r1 & r1 in ( dom f) holds |.((f . r1) - g).| < g1

      proof

        assume

         A1: f is convergent_in+infty;

        then

        consider g2 such that

         A2: for seq st seq is divergent_to+infty & ( rng seq) c= ( dom f) holds (f /* seq) is convergent & ( lim (f /* seq)) = g2;

        assume not (for r holds ex g st r < g & g in ( dom f)) or for g holds ex g1 st 0 < g1 & for r holds ex r1 st r < r1 & r1 in ( dom f) & |.((f . r1) - g).| >= g1;

        then

        consider g such that

         A3: 0 < g and

         A4: for r holds ex r1 st r < r1 & r1 in ( dom f) & |.((f . r1) - g2).| >= g by A1;

        defpred X[ Nat, Real] means $1 < $2 & $2 in ( dom f) & |.((f . $2) - g2).| >= g;

        

         A5: for n be Element of NAT holds ex r be Element of REAL st X[n, r]

        proof

          let n be Element of NAT ;

          consider r such that

           A6: X[n, r] by A4;

          reconsider r as Real;

           X[n, r] by A6;

          hence thesis;

        end;

        consider s be Real_Sequence such that

         A7: for n be Element of NAT holds X[n, (s . n)] from FUNCT_2:sch 3( A5);

        now

          let x be object;

          assume x in ( rng s);

          then ex n be Element of NAT st (s . n) = x by FUNCT_2: 113;

          hence x in ( dom f) by A7;

        end;

        then

         A8: ( rng s) c= ( dom f);

        now

          let n;

          

           A9: n in NAT by ORDINAL1:def 12;

          then n < (s . n) by A7;

          hence (s1 . n) <= (s . n) by FUNCT_1: 18, A9;

        end;

        then s is divergent_to+infty by Lm5, Th20, Th42;

        then (f /* s) is convergent & ( lim (f /* s)) = g2 by A2, A8;

        then

        consider n such that

         A10: for m st n <= m holds |.(((f /* s) . m) - g2).| < g by A3, SEQ_2:def 7;

        

         A11: n in NAT by ORDINAL1:def 12;

         |.(((f /* s) . n) - g2).| < g by A10;

        then |.((f . (s . n)) - g2).| < g by A8, FUNCT_2: 108, A11;

        hence contradiction by A7, A11;

      end;

      assume

       A12: for r holds ex g st r < g & g in ( dom f);

      given g such that

       A13: for g1 st 0 < g1 holds ex r st for r1 st r < r1 & r1 in ( dom f) holds |.((f . r1) - g).| < g1;

      now

        let s be Real_Sequence such that

         A14: s is divergent_to+infty and

         A15: ( rng s) c= ( dom f);

         A16:

        now

          let g1 be Real;

          assume

           A17: 0 < g1;

          consider r such that

           A18: for r1 st r < r1 & r1 in ( dom f) holds |.((f . r1) - g).| < g1 by A13, A17;

          consider n such that

           A19: for m st n <= m holds r < (s . m) by A14;

          take n;

          let m;

          

           A20: (s . m) in ( rng s) by VALUED_0: 28;

          

           A21: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then |.((f . (s . m)) - g).| < g1 by A15, A18, A19, A20;

          hence |.(((f /* s) . m) - g).| < g1 by A15, FUNCT_2: 108, A21;

        end;

        hence (f /* s) is convergent;

        hence ( lim (f /* s)) = g by A16, SEQ_2:def 7;

      end;

      hence thesis by A12;

    end;

    theorem :: LIMFUNC1:45

    f is convergent_in-infty iff (for r holds ex g st g < r & g in ( dom f)) & ex g st for g1 st 0 < g1 holds ex r st for r1 st r1 < r & r1 in ( dom f) holds |.((f . r1) - g).| < g1

    proof

      thus f is convergent_in-infty implies (for r holds ex g st g < r & g in ( dom f)) & ex g st for g1 st 0 < g1 holds ex r st for r1 st r1 < r & r1 in ( dom f) holds |.((f . r1) - g).| < g1

      proof

        assume

         A1: f is convergent_in-infty;

        then

        consider g2 such that

         A2: for seq st seq is divergent_to-infty & ( rng seq) c= ( dom f) holds (f /* seq) is convergent & ( lim (f /* seq)) = g2;

        assume not (for r holds ex g st g < r & g in ( dom f)) or for g holds ex g1 st 0 < g1 & for r holds ex r1 st r1 < r & r1 in ( dom f) & |.((f . r1) - g).| >= g1;

        then

        consider g such that

         A3: 0 < g and

         A4: for r holds ex r1 st r1 < r & r1 in ( dom f) & |.((f . r1) - g2).| >= g by A1;

        defpred X[ Nat, Real] means $2 < ( - $1) & $2 in ( dom f) & |.((f . $2) - g2).| >= g;

        

         A5: for n be Element of NAT holds ex r be Element of REAL st X[n, r]

        proof

          let n be Element of NAT ;

          consider r such that

           A6: X[n, r] by A4;

          reconsider r as Real;

           X[n, r] by A6;

          hence thesis;

        end;

        consider s be Real_Sequence such that

         A7: for n be Element of NAT holds X[n, (s . n)] from FUNCT_2:sch 3( A5);

        now

          let x be object;

          assume x in ( rng s);

          then ex n be Element of NAT st (s . n) = x by FUNCT_2: 113;

          hence x in ( dom f) by A7;

        end;

        then

         A8: ( rng s) c= ( dom f);

        deffunc U( Nat) = ( - $1);

        consider s1 be Real_Sequence such that

         A9: for n holds (s1 . n) = U(n) from SEQ_1:sch 1;

        now

          let n;

          n in NAT by ORDINAL1:def 12;

          then (s . n) < ( - n) by A7;

          hence (s . n) <= (s1 . n) by A9;

        end;

        then s is divergent_to-infty by A9, Th21, Th43;

        then (f /* s) is convergent & ( lim (f /* s)) = g2 by A2, A8;

        then

        consider n such that

         A10: for m st n <= m holds |.(((f /* s) . m) - g2).| < g by A3, SEQ_2:def 7;

        

         A11: n in NAT by ORDINAL1:def 12;

         |.(((f /* s) . n) - g2).| < g by A10;

        then |.((f . (s . n)) - g2).| < g by A8, FUNCT_2: 108, A11;

        hence contradiction by A7, A11;

      end;

      assume

       A12: for r holds ex g st g < r & g in ( dom f);

      given g such that

       A13: for g1 st 0 < g1 holds ex r st for r1 st r1 < r & r1 in ( dom f) holds |.((f . r1) - g).| < g1;

      now

        let s be Real_Sequence such that

         A14: s is divergent_to-infty and

         A15: ( rng s) c= ( dom f);

         A16:

        now

          let g1 be Real;

          assume

           A17: 0 < g1;

          consider r such that

           A18: for r1 st r1 < r & r1 in ( dom f) holds |.((f . r1) - g).| < g1 by A13, A17;

          consider n such that

           A19: for m st n <= m holds (s . m) < r by A14;

          take n;

          let m;

          

           A20: (s . m) in ( rng s) by VALUED_0: 28;

          

           A21: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then |.((f . (s . m)) - g).| < g1 by A15, A18, A19, A20;

          hence |.(((f /* s) . m) - g).| < g1 by A15, FUNCT_2: 108, A21;

        end;

        hence (f /* s) is convergent;

        hence ( lim (f /* s)) = g by A16, SEQ_2:def 7;

      end;

      hence thesis by A12;

    end;

    theorem :: LIMFUNC1:46

    f is divergent_in+infty_to+infty iff (for r holds ex g st r < g & g in ( dom f)) & for g holds ex r st for r1 st r < r1 & r1 in ( dom f) holds g < (f . r1)

    proof

      thus f is divergent_in+infty_to+infty implies (for r holds ex g st r < g & g in ( dom f)) & for g holds ex r st for r1 st r < r1 & r1 in ( dom f) holds g < (f . r1)

      proof

        assume

         A1: f is divergent_in+infty_to+infty;

        assume not (for r holds ex g st r < g & g in ( dom f)) or ex g st for r holds ex r1 st r < r1 & r1 in ( dom f) & g >= (f . r1);

        then

        consider g such that

         A2: for r holds ex r1 st r < r1 & r1 in ( dom f) & g >= (f . r1) by A1;

        defpred X[ Nat, Real] means $1 < $2 & $2 in ( dom f) & g >= (f . $2);

        

         A3: for n be Element of NAT holds ex r be Element of REAL st X[n, r]

        proof

          let n be Element of NAT ;

          consider r such that

           A4: X[n, r] by A2;

          reconsider r as Real;

           X[n, r] by A4;

          hence thesis;

        end;

        consider s be Real_Sequence such that

         A5: for n be Element of NAT holds X[n, (s . n)] from FUNCT_2:sch 3( A3);

        now

          let x be object;

          assume x in ( rng s);

          then ex n be Element of NAT st (s . n) = x by FUNCT_2: 113;

          hence x in ( dom f) by A5;

        end;

        then

         A6: ( rng s) c= ( dom f);

        now

          let n;

          

           A7: n in NAT by ORDINAL1:def 12;

          n < (s . n) by A5, A7;

          hence (s1 . n) <= (s . n) by FUNCT_1: 18, A7;

        end;

        then s is divergent_to+infty by Lm5, Th20, Th42;

        then (f /* s) is divergent_to+infty by A1, A6;

        then

        consider n such that

         A8: for m st n <= m holds g < ((f /* s) . m);

        

         A9: n in NAT by ORDINAL1:def 12;

        g < ((f /* s) . n) by A8;

        then g < (f . (s . n)) by A6, FUNCT_2: 108, A9;

        hence contradiction by A5, A9;

      end;

      assume that

       A10: for r holds ex g st r < g & g in ( dom f) and

       A11: for g holds ex r st for r1 st r < r1 & r1 in ( dom f) holds g < (f . r1);

      now

        let s be Real_Sequence such that

         A12: s is divergent_to+infty and

         A13: ( rng s) c= ( dom f);

        now

          let g;

          consider r such that

           A14: for r1 st r < r1 & r1 in ( dom f) holds g < (f . r1) by A11;

          consider n such that

           A15: for m st n <= m holds r < (s . m) by A12;

          take n;

          let m;

          

           A16: (s . m) in ( rng s) by VALUED_0: 28;

          

           A17: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then g < (f . (s . m)) by A13, A14, A15, A16;

          hence g < ((f /* s) . m) by A13, FUNCT_2: 108, A17;

        end;

        hence (f /* s) is divergent_to+infty;

      end;

      hence thesis by A10;

    end;

    theorem :: LIMFUNC1:47

    f is divergent_in+infty_to-infty iff (for r holds ex g st r < g & g in ( dom f)) & for g holds ex r st for r1 st r < r1 & r1 in ( dom f) holds (f . r1) < g

    proof

      thus f is divergent_in+infty_to-infty implies (for r holds ex g st r < g & g in ( dom f)) & for g holds ex r st for r1 st r < r1 & r1 in ( dom f) holds (f . r1) < g

      proof

        assume

         A1: f is divergent_in+infty_to-infty;

        assume not (for r holds ex g st r < g & g in ( dom f)) or ex g st for r holds ex r1 st r < r1 & r1 in ( dom f) & (f . r1) >= g;

        then

        consider g such that

         A2: for r holds ex r1 st r < r1 & r1 in ( dom f) & (f . r1) >= g by A1;

        defpred X[ Nat, Real] means $1 < $2 & $2 in ( dom f) & g <= (f . $2);

        

         A3: for n be Element of NAT holds ex r be Element of REAL st X[n, r]

        proof

          let n be Element of NAT ;

          consider r such that

           A4: X[n, r] by A2;

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

           X[n, r] by A4;

          hence thesis;

        end;

        consider s be Real_Sequence such that

         A5: for n be Element of NAT holds X[n, (s . n)] from FUNCT_2:sch 3( A3);

        now

          let x be object;

          assume x in ( rng s);

          then ex n be Element of NAT st (s . n) = x by FUNCT_2: 113;

          hence x in ( dom f) by A5;

        end;

        then

         A6: ( rng s) c= ( dom f);

        now

          let n;

          

           A7: n in NAT by ORDINAL1:def 12;

          n < (s . n) by A5, A7;

          hence (s1 . n) <= (s . n) by FUNCT_1: 18, A7;

        end;

        then s is divergent_to+infty by Lm5, Th20, Th42;

        then (f /* s) is divergent_to-infty by A1, A6;

        then

        consider n such that

         A8: for m st n <= m holds ((f /* s) . m) < g;

        

         A9: n in NAT by ORDINAL1:def 12;

        ((f /* s) . n) < g by A8;

        then (f . (s . n)) < g by A6, FUNCT_2: 108, A9;

        hence contradiction by A5, A9;

      end;

      assume that

       A10: for r holds ex g st r < g & g in ( dom f) and

       A11: for g holds ex r st for r1 st r < r1 & r1 in ( dom f) holds (f . r1) < g;

      now

        let s be Real_Sequence such that

         A12: s is divergent_to+infty and

         A13: ( rng s) c= ( dom f);

        now

          let g;

          consider r such that

           A14: for r1 st r < r1 & r1 in ( dom f) holds (f . r1) < g by A11;

          consider n such that

           A15: for m st n <= m holds r < (s . m) by A12;

          take n;

          let m;

          

           A16: (s . m) in ( rng s) by VALUED_0: 28;

          

           A17: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then (f . (s . m)) < g by A13, A14, A15, A16;

          hence ((f /* s) . m) < g by A13, FUNCT_2: 108, A17;

        end;

        hence (f /* s) is divergent_to-infty;

      end;

      hence thesis by A10;

    end;

    theorem :: LIMFUNC1:48

    f is divergent_in-infty_to+infty iff (for r holds ex g st g < r & g in ( dom f)) & for g holds ex r st for r1 st r1 < r & r1 in ( dom f) holds g < (f . r1)

    proof

      thus f is divergent_in-infty_to+infty implies (for r holds ex g st g < r & g in ( dom f)) & for g holds ex r st for r1 st r1 < r & r1 in ( dom f) holds g < (f . r1)

      proof

        deffunc U( Nat) = ( - $1);

        assume

         A1: f is divergent_in-infty_to+infty;

        assume not (for r holds ex g st g < r & g in ( dom f)) or ex g st for r holds ex r1 st r1 < r & r1 in ( dom f) & g >= (f . r1);

        then

        consider g such that

         A2: for r holds ex r1 st r1 < r & r1 in ( dom f) & g >= (f . r1) by A1;

        defpred X[ Nat, Real] means $2 < ( - $1) & $2 in ( dom f) & g >= (f . $2);

        

         A3: for n be Element of NAT holds ex r be Element of REAL st X[n, r]

        proof

          let n be Element of NAT ;

          consider r such that

           A4: X[n, r] by A2;

          reconsider r as Real;

           X[n, r] by A4;

          hence thesis;

        end;

        consider s be Real_Sequence such that

         A5: for n be Element of NAT holds X[n, (s . n)] from FUNCT_2:sch 3( A3);

        now

          let x be object;

          assume x in ( rng s);

          then ex n be Element of NAT st (s . n) = x by FUNCT_2: 113;

          hence x in ( dom f) by A5;

        end;

        then

         A6: ( rng s) c= ( dom f);

        consider s1 be Real_Sequence such that

         A7: for n holds (s1 . n) = U(n) from SEQ_1:sch 1;

        now

          let n;

          

           A8: n in NAT by ORDINAL1:def 12;

          (s . n) < ( - n) by A5, A8;

          hence (s . n) <= (s1 . n) by A7;

        end;

        then s is divergent_to-infty by A7, Th21, Th43;

        then (f /* s) is divergent_to+infty by A1, A6;

        then

        consider n such that

         A9: for m st n <= m holds g < ((f /* s) . m);

        

         A10: n in NAT by ORDINAL1:def 12;

        g < ((f /* s) . n) by A9;

        then g < (f . (s . n)) by A6, FUNCT_2: 108, A10;

        hence contradiction by A5, A10;

      end;

      assume that

       A11: for r holds ex g st g < r & g in ( dom f) and

       A12: for g holds ex r st for r1 st r1 < r & r1 in ( dom f) holds g < (f . r1);

      now

        let s be Real_Sequence such that

         A13: s is divergent_to-infty and

         A14: ( rng s) c= ( dom f);

        now

          let g;

          consider r such that

           A15: for r1 st r1 < r & r1 in ( dom f) holds g < (f . r1) by A12;

          consider n such that

           A16: for m st n <= m holds (s . m) < r by A13;

          take n;

          let m;

          

           A17: (s . m) in ( rng s) by VALUED_0: 28;

          

           A18: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then g < (f . (s . m)) by A14, A15, A16, A17;

          hence g < ((f /* s) . m) by A14, FUNCT_2: 108, A18;

        end;

        hence (f /* s) is divergent_to+infty;

      end;

      hence thesis by A11;

    end;

    theorem :: LIMFUNC1:49

    f is divergent_in-infty_to-infty iff (for r holds ex g st g < r & g in ( dom f)) & for g holds ex r st for r1 st r1 < r & r1 in ( dom f) holds (f . r1) < g

    proof

      thus f is divergent_in-infty_to-infty implies (for r holds ex g st g < r & g in ( dom f)) & for g holds ex r st for r1 st r1 < r & r1 in ( dom f) holds (f . r1) < g

      proof

        deffunc U( Nat) = ( - $1);

        assume

         A1: f is divergent_in-infty_to-infty;

        assume not (for r holds ex g st g < r & g in ( dom f)) or ex g st for r holds ex r1 st r1 < r & r1 in ( dom f) & (f . r1) >= g;

        then

        consider g such that

         A2: for r holds ex r1 st r1 < r & r1 in ( dom f) & (f . r1) >= g by A1;

        defpred X[ Nat, Real] means $2 < ( - $1) & $2 in ( dom f) & g <= (f . $2);

        

         A3: for n be Element of NAT holds ex r be Element of REAL st X[n, r]

        proof

          let n be Element of NAT ;

          consider r such that

           A4: X[n, r] by A2;

          reconsider r as Real;

           X[n, r] by A4;

          hence thesis;

        end;

        consider s be Real_Sequence such that

         A5: for n be Element of NAT holds X[n, (s . n)] from FUNCT_2:sch 3( A3);

        now

          let x be object;

          assume x in ( rng s);

          then ex n be Element of NAT st (s . n) = x by FUNCT_2: 113;

          hence x in ( dom f) by A5;

        end;

        then

         A6: ( rng s) c= ( dom f);

        consider s1 be Real_Sequence such that

         A7: for n holds (s1 . n) = U(n) from SEQ_1:sch 1;

        now

          let n;

          

           A8: n in NAT by ORDINAL1:def 12;

          (s . n) < ( - n) by A5, A8;

          hence (s . n) <= (s1 . n) by A7;

        end;

        then s is divergent_to-infty by A7, Th21, Th43;

        then (f /* s) is divergent_to-infty by A1, A6;

        then

        consider n such that

         A9: for m st n <= m holds ((f /* s) . m) < g;

        

         A10: n in NAT by ORDINAL1:def 12;

        ((f /* s) . n) < g by A9;

        then (f . (s . n)) < g by A6, FUNCT_2: 108, A10;

        hence contradiction by A5, A10;

      end;

      assume that

       A11: for r holds ex g st g < r & g in ( dom f) and

       A12: for g holds ex r st for r1 st r1 < r & r1 in ( dom f) holds (f . r1) < g;

      now

        let s be Real_Sequence such that

         A13: s is divergent_to-infty and

         A14: ( rng s) c= ( dom f);

        now

          let g;

          consider r such that

           A15: for r1 st r1 < r & r1 in ( dom f) holds (f . r1) < g by A12;

          consider n such that

           A16: for m st n <= m holds (s . m) < r by A13;

          take n;

          let m;

          

           A17: (s . m) in ( rng s) by VALUED_0: 28;

          

           A18: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then (f . (s . m)) < g by A14, A15, A16, A17;

          hence ((f /* s) . m) < g by A14, FUNCT_2: 108, A18;

        end;

        hence (f /* s) is divergent_to-infty;

      end;

      hence thesis by A11;

    end;

    theorem :: LIMFUNC1:50

    f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to+infty & (for r holds ex g st r < g & g in (( dom f1) /\ ( dom f2))) implies (f1 + f2) is divergent_in+infty_to+infty & (f1 (#) f2) is divergent_in+infty_to+infty

    proof

      assume that

       A1: f1 is divergent_in+infty_to+infty and

       A2: f2 is divergent_in+infty_to+infty and

       A3: for r holds ex g st r < g & g in (( dom f1) /\ ( dom f2));

       A4:

      now

        let seq;

        assume that

         A5: seq is divergent_to+infty and

         A6: ( rng seq) c= ( dom (f1 + f2));

        

         A7: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by A6, Lm2;

        ( rng seq) c= ( dom f2) by A6, Lm2;

        then

         A8: (f2 /* seq) is divergent_to+infty by A2, A5;

        ( rng seq) c= ( dom f1) by A6, Lm2;

        then (f1 /* seq) is divergent_to+infty by A1, A5;

        then ((f1 /* seq) + (f2 /* seq)) is divergent_to+infty by A8, Th8;

        hence ((f1 + f2) /* seq) is divergent_to+infty by A6, A7, RFUNCT_2: 8;

      end;

       A9:

      now

        let seq;

        assume that

         A10: seq is divergent_to+infty and

         A11: ( rng seq) c= ( dom (f1 (#) f2));

        

         A12: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by A11, Lm3;

        ( rng seq) c= ( dom f2) by A11, Lm3;

        then

         A13: (f2 /* seq) is divergent_to+infty by A2, A10;

        ( rng seq) c= ( dom f1) by A11, Lm3;

        then (f1 /* seq) is divergent_to+infty by A1, A10;

        then ((f1 /* seq) (#) (f2 /* seq)) is divergent_to+infty by A13, Th10;

        hence ((f1 (#) f2) /* seq) is divergent_to+infty by A11, A12, RFUNCT_2: 8;

      end;

      now

        let r;

        consider g such that

         A14: r < g & g in (( dom f1) /\ ( dom f2)) by A3;

        take g;

        thus r < g & g in ( dom (f1 + f2)) by A14, VALUED_1:def 1;

      end;

      hence (f1 + f2) is divergent_in+infty_to+infty by A4;

      now

        let r;

        consider g such that

         A15: r < g & g in (( dom f1) /\ ( dom f2)) by A3;

        take g;

        thus r < g & g in ( dom (f1 (#) f2)) by A15, VALUED_1:def 4;

      end;

      hence thesis by A9;

    end;

    theorem :: LIMFUNC1:51

    f1 is divergent_in+infty_to-infty & f2 is divergent_in+infty_to-infty & (for r holds ex g st r < g & g in (( dom f1) /\ ( dom f2))) implies (f1 + f2) is divergent_in+infty_to-infty & (f1 (#) f2) is divergent_in+infty_to+infty

    proof

      assume that

       A1: f1 is divergent_in+infty_to-infty and

       A2: f2 is divergent_in+infty_to-infty and

       A3: for r holds ex g st r < g & g in (( dom f1) /\ ( dom f2));

       A4:

      now

        let seq;

        assume that

         A5: seq is divergent_to+infty and

         A6: ( rng seq) c= ( dom (f1 + f2));

        

         A7: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by A6, Lm2;

        ( rng seq) c= ( dom f2) by A6, Lm2;

        then

         A8: (f2 /* seq) is divergent_to-infty by A2, A5;

        ( rng seq) c= ( dom f1) by A6, Lm2;

        then (f1 /* seq) is divergent_to-infty by A1, A5;

        then ((f1 /* seq) + (f2 /* seq)) is divergent_to-infty by A8, Th11;

        hence ((f1 + f2) /* seq) is divergent_to-infty by A6, A7, RFUNCT_2: 8;

      end;

       A9:

      now

        let seq;

        assume that

         A10: seq is divergent_to+infty and

         A11: ( rng seq) c= ( dom (f1 (#) f2));

        

         A12: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by A11, Lm3;

        ( rng seq) c= ( dom f2) by A11, Lm3;

        then

         A13: (f2 /* seq) is divergent_to-infty by A2, A10;

        ( rng seq) c= ( dom f1) by A11, Lm3;

        then (f1 /* seq) is divergent_to-infty by A1, A10;

        then ((f1 /* seq) (#) (f2 /* seq)) is divergent_to+infty by A13, Th24;

        hence ((f1 (#) f2) /* seq) is divergent_to+infty by A11, A12, RFUNCT_2: 8;

      end;

      now

        let r;

        consider g such that

         A14: r < g & g in (( dom f1) /\ ( dom f2)) by A3;

        take g;

        thus r < g & g in ( dom (f1 + f2)) by A14, VALUED_1:def 1;

      end;

      hence (f1 + f2) is divergent_in+infty_to-infty by A4;

      now

        let r;

        consider g such that

         A15: r < g & g in (( dom f1) /\ ( dom f2)) by A3;

        take g;

        thus r < g & g in ( dom (f1 (#) f2)) by A15, VALUED_1:def 4;

      end;

      hence thesis by A9;

    end;

    theorem :: LIMFUNC1:52

    f1 is divergent_in-infty_to+infty & f2 is divergent_in-infty_to+infty & (for r holds ex g st g < r & g in (( dom f1) /\ ( dom f2))) implies (f1 + f2) is divergent_in-infty_to+infty & (f1 (#) f2) is divergent_in-infty_to+infty

    proof

      assume that

       A1: f1 is divergent_in-infty_to+infty and

       A2: f2 is divergent_in-infty_to+infty and

       A3: for r holds ex g st g < r & g in (( dom f1) /\ ( dom f2));

       A4:

      now

        let seq;

        assume that

         A5: seq is divergent_to-infty and

         A6: ( rng seq) c= ( dom (f1 + f2));

        

         A7: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by A6, Lm2;

        ( rng seq) c= ( dom f2) by A6, Lm2;

        then

         A8: (f2 /* seq) is divergent_to+infty by A2, A5;

        ( rng seq) c= ( dom f1) by A6, Lm2;

        then (f1 /* seq) is divergent_to+infty by A1, A5;

        then ((f1 /* seq) + (f2 /* seq)) is divergent_to+infty by A8, Th8;

        hence ((f1 + f2) /* seq) is divergent_to+infty by A6, A7, RFUNCT_2: 8;

      end;

       A9:

      now

        let seq;

        assume that

         A10: seq is divergent_to-infty and

         A11: ( rng seq) c= ( dom (f1 (#) f2));

        

         A12: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by A11, Lm3;

        ( rng seq) c= ( dom f2) by A11, Lm3;

        then

         A13: (f2 /* seq) is divergent_to+infty by A2, A10;

        ( rng seq) c= ( dom f1) by A11, Lm3;

        then (f1 /* seq) is divergent_to+infty by A1, A10;

        then ((f1 /* seq) (#) (f2 /* seq)) is divergent_to+infty by A13, Th10;

        hence ((f1 (#) f2) /* seq) is divergent_to+infty by A11, A12, RFUNCT_2: 8;

      end;

      now

        let r;

        consider g such that

         A14: g < r & g in (( dom f1) /\ ( dom f2)) by A3;

        take g;

        thus g < r & g in ( dom (f1 + f2)) by A14, VALUED_1:def 1;

      end;

      hence (f1 + f2) is divergent_in-infty_to+infty by A4;

      now

        let r;

        consider g such that

         A15: g < r & g in (( dom f1) /\ ( dom f2)) by A3;

        take g;

        thus g < r & g in ( dom (f1 (#) f2)) by A15, VALUED_1:def 4;

      end;

      hence thesis by A9;

    end;

    theorem :: LIMFUNC1:53

    f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to-infty & (for r holds ex g st g < r & g in (( dom f1) /\ ( dom f2))) implies (f1 + f2) is divergent_in-infty_to-infty & (f1 (#) f2) is divergent_in-infty_to+infty

    proof

      assume that

       A1: f1 is divergent_in-infty_to-infty and

       A2: f2 is divergent_in-infty_to-infty and

       A3: for r holds ex g st g < r & g in (( dom f1) /\ ( dom f2));

       A4:

      now

        let seq;

        assume that

         A5: seq is divergent_to-infty and

         A6: ( rng seq) c= ( dom (f1 + f2));

        

         A7: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by A6, Lm2;

        ( rng seq) c= ( dom f2) by A6, Lm2;

        then

         A8: (f2 /* seq) is divergent_to-infty by A2, A5;

        ( rng seq) c= ( dom f1) by A6, Lm2;

        then (f1 /* seq) is divergent_to-infty by A1, A5;

        then ((f1 /* seq) + (f2 /* seq)) is divergent_to-infty by A8, Th11;

        hence ((f1 + f2) /* seq) is divergent_to-infty by A6, A7, RFUNCT_2: 8;

      end;

       A9:

      now

        let seq;

        assume that

         A10: seq is divergent_to-infty and

         A11: ( rng seq) c= ( dom (f1 (#) f2));

        

         A12: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by A11, Lm3;

        ( rng seq) c= ( dom f2) by A11, Lm3;

        then

         A13: (f2 /* seq) is divergent_to-infty by A2, A10;

        ( rng seq) c= ( dom f1) by A11, Lm3;

        then (f1 /* seq) is divergent_to-infty by A1, A10;

        then ((f1 /* seq) (#) (f2 /* seq)) is divergent_to+infty by A13, Th24;

        hence ((f1 (#) f2) /* seq) is divergent_to+infty by A11, A12, RFUNCT_2: 8;

      end;

      now

        let r;

        consider g such that

         A14: g < r & g in (( dom f1) /\ ( dom f2)) by A3;

        take g;

        thus g < r & g in ( dom (f1 + f2)) by A14, VALUED_1:def 1;

      end;

      hence (f1 + f2) is divergent_in-infty_to-infty by A4;

      now

        let r;

        consider g such that

         A15: g < r & g in (( dom f1) /\ ( dom f2)) by A3;

        take g;

        thus g < r & g in ( dom (f1 (#) f2)) by A15, VALUED_1:def 4;

      end;

      hence thesis by A9;

    end;

    theorem :: LIMFUNC1:54

    f1 is divergent_in+infty_to+infty & (for r holds ex g st r < g & g in ( dom (f1 + f2))) & (ex r st (f2 | ( right_open_halfline r)) is bounded_below) implies (f1 + f2) is divergent_in+infty_to+infty

    proof

      assume that

       A1: f1 is divergent_in+infty_to+infty and

       A2: for r holds ex g st r < g & g in ( dom (f1 + f2));

      given r1 such that

       A3: (f2 | ( right_open_halfline r1)) is bounded_below;

      now

        let seq;

        assume that

         A4: seq is divergent_to+infty and

         A5: ( rng seq) c= ( dom (f1 + f2));

        consider k such that

         A6: for n st k <= n holds r1 < (seq . n) by A4;

        

         A7: ( rng (seq ^\ k)) c= ( rng seq) by VALUED_0: 21;

        ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by A5, Lm2;

        then ( rng (seq ^\ k)) c= (( dom f1) /\ ( dom f2)) by A5, A7;

        

        then

         A8: ((f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k))) = ((f1 + f2) /* (seq ^\ k)) by RFUNCT_2: 8

        .= (((f1 + f2) /* seq) ^\ k) by A5, VALUED_0: 27;

        consider r2 be Real such that

         A9: for g be object st g in (( right_open_halfline r1) /\ ( dom f2)) holds r2 <= (f2 . g) by A3, RFUNCT_1: 71;

        

         A10: ( rng seq) c= ( dom f2) by A5, Lm2;

        then

         A11: ( rng (seq ^\ k)) c= ( dom f2) by A7;

        now

          let n;

          

           A12: n in NAT by ORDINAL1:def 12;

          reconsider nk = (n + k), nn = n as Element of NAT by ORDINAL1:def 12;

          r1 < (seq . nk) by A6, NAT_1: 12;

          then ((seq ^\ k) . nn) < +infty & r1 < ((seq ^\ k) . nn) by NAT_1:def 3, XXREAL_0: 9;

          then ((seq ^\ k) . n) in ( rng (seq ^\ k)) & ((seq ^\ k) . n) in ( right_open_halfline r1) by VALUED_0: 28, XXREAL_1: 4;

          then ((seq ^\ k) . n) in (( right_open_halfline r1) /\ ( dom f2)) by A11, XBOOLE_0:def 4;

          then r2 <= (f2 . ((seq ^\ k) . n)) by A9;

          then

           A13: r2 <= ((f2 /* (seq ^\ k)) . n) by A10, A7, FUNCT_2: 108, XBOOLE_1: 1, A12;

          ( - |.r2.|) <= r2 by ABSVALUE: 4;

          then (( - |.r2.|) - 1) < (r2 - 0 ) by XREAL_1: 15;

          hence (( - |.r2.|) - 1) < ((f2 /* (seq ^\ k)) . n) by A13, XXREAL_0: 2;

        end;

        then

         A14: (f2 /* (seq ^\ k)) is bounded_below;

        ( rng seq) c= ( dom f1) by A5, Lm2;

        then

         A15: ( rng (seq ^\ k)) c= ( dom f1) by A7;

        (seq ^\ k) is divergent_to+infty by A4, Th26;

        then (f1 /* (seq ^\ k)) is divergent_to+infty by A1, A15;

        then ((f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k))) is divergent_to+infty by A14, Th9;

        hence ((f1 + f2) /* seq) is divergent_to+infty by A8, Th7;

      end;

      hence thesis by A2;

    end;

    theorem :: LIMFUNC1:55

    f1 is divergent_in+infty_to+infty & (for r holds ex g st r < g & g in ( dom (f1 (#) f2))) & (ex r, r1 st 0 < r & for g st g in (( dom f2) /\ ( right_open_halfline r1)) holds r <= (f2 . g)) implies (f1 (#) f2) is divergent_in+infty_to+infty

    proof

      assume that

       A1: f1 is divergent_in+infty_to+infty and

       A2: for r holds ex g st r < g & g in ( dom (f1 (#) f2));

      given r2, r1 such that

       A3: 0 < r2 and

       A4: for g st g in (( dom f2) /\ ( right_open_halfline r1)) holds r2 <= (f2 . g);

      now

        let seq;

        assume that

         A5: seq is divergent_to+infty and

         A6: ( rng seq) c= ( dom (f1 (#) f2));

        consider k such that

         A7: for n st k <= n holds r1 < (seq . n) by A5;

        

         A8: ( rng (seq ^\ k)) c= ( rng seq) by VALUED_0: 21;

        

         A9: ( rng seq) c= ( dom f2) by A6, Lm3;

        then

         A10: ( rng (seq ^\ k)) c= ( dom f2) by A8;

         A11:

        now

          thus 0 < r2 by A3;

          let n;

          

           A12: n in NAT by ORDINAL1:def 12;

          r1 < (seq . (n + k)) by A7, NAT_1: 12;

          then r1 < ((seq ^\ k) . n) by NAT_1:def 3;

          then ((seq ^\ k) . n) in { g2 : r1 < g2 };

          then ((seq ^\ k) . n) in ( rng (seq ^\ k)) & ((seq ^\ k) . n) in ( right_open_halfline r1) by VALUED_0: 28, XXREAL_1: 230;

          then ((seq ^\ k) . n) in (( dom f2) /\ ( right_open_halfline r1)) by A10, XBOOLE_0:def 4;

          then r2 <= (f2 . ((seq ^\ k) . n)) by A4;

          hence r2 <= ((f2 /* (seq ^\ k)) . n) by A9, A8, FUNCT_2: 108, XBOOLE_1: 1, A12;

        end;

        ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by A6, Lm3;

        then ( rng (seq ^\ k)) c= (( dom f1) /\ ( dom f2)) by A6, A8;

        

        then

         A13: ((f1 /* (seq ^\ k)) (#) (f2 /* (seq ^\ k))) = ((f1 (#) f2) /* (seq ^\ k)) by RFUNCT_2: 8

        .= (((f1 (#) f2) /* seq) ^\ k) by A6, VALUED_0: 27;

        ( rng seq) c= ( dom f1) by A6, Lm3;

        then

         A14: ( rng (seq ^\ k)) c= ( dom f1) by A8;

        (seq ^\ k) is divergent_to+infty by A5, Th26;

        then (f1 /* (seq ^\ k)) is divergent_to+infty by A1, A14;

        then ((f1 /* (seq ^\ k)) (#) (f2 /* (seq ^\ k))) is divergent_to+infty by A11, Th22;

        hence ((f1 (#) f2) /* seq) is divergent_to+infty by A13, Th7;

      end;

      hence thesis by A2;

    end;

    theorem :: LIMFUNC1:56

    f1 is divergent_in-infty_to+infty & (for r holds ex g st g < r & g in ( dom (f1 + f2))) & (ex r st (f2 | ( left_open_halfline r)) is bounded_below) implies (f1 + f2) is divergent_in-infty_to+infty

    proof

      assume that

       A1: f1 is divergent_in-infty_to+infty and

       A2: for r holds ex g st g < r & g in ( dom (f1 + f2));

      given r1 such that

       A3: (f2 | ( left_open_halfline r1)) is bounded_below;

      now

        let seq;

        assume that

         A4: seq is divergent_to-infty and

         A5: ( rng seq) c= ( dom (f1 + f2));

        consider k such that

         A6: for n st k <= n holds (seq . n) < r1 by A4;

        

         A7: ( rng (seq ^\ k)) c= ( rng seq) by VALUED_0: 21;

        ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by A5, Lm2;

        then ( rng (seq ^\ k)) c= (( dom f1) /\ ( dom f2)) by A5, A7;

        

        then

         A8: ((f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k))) = ((f1 + f2) /* (seq ^\ k)) by RFUNCT_2: 8

        .= (((f1 + f2) /* seq) ^\ k) by A5, VALUED_0: 27;

        consider r2 be Real such that

         A9: for g be object st g in (( left_open_halfline r1) /\ ( dom f2)) holds r2 <= (f2 . g) by A3, RFUNCT_1: 71;

        

         A10: ( rng seq) c= ( dom f2) by A5, Lm2;

        then

         A11: ( rng (seq ^\ k)) c= ( dom f2) by A7;

        now

          let n;

          

           A12: n in NAT by ORDINAL1:def 12;

          (seq . (n + k)) < r1 by A6, NAT_1: 12;

          then ((seq ^\ k) . n) < r1 by NAT_1:def 3;

          then ((seq ^\ k) . n) in { g2 : g2 < r1 };

          then ((seq ^\ k) . n) in ( rng (seq ^\ k)) & ((seq ^\ k) . n) in ( left_open_halfline r1) by VALUED_0: 28, XXREAL_1: 229;

          then ((seq ^\ k) . n) in (( left_open_halfline r1) /\ ( dom f2)) by A11, XBOOLE_0:def 4;

          then r2 <= (f2 . ((seq ^\ k) . n)) by A9;

          then

           A13: r2 <= ((f2 /* (seq ^\ k)) . n) by A10, A7, FUNCT_2: 108, XBOOLE_1: 1, A12;

          ( - |.r2.|) <= r2 by ABSVALUE: 4;

          then (( - |.r2.|) - 1) < (r2 - 0 ) by XREAL_1: 15;

          hence (( - |.r2.|) - 1) < ((f2 /* (seq ^\ k)) . n) by A13, XXREAL_0: 2;

        end;

        then

         A14: (f2 /* (seq ^\ k)) is bounded_below;

        ( rng seq) c= ( dom f1) by A5, Lm2;

        then

         A15: ( rng (seq ^\ k)) c= ( dom f1) by A7;

        (seq ^\ k) is divergent_to-infty by A4, Th27;

        then (f1 /* (seq ^\ k)) is divergent_to+infty by A1, A15;

        then ((f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k))) is divergent_to+infty by A14, Th9;

        hence ((f1 + f2) /* seq) is divergent_to+infty by A8, Th7;

      end;

      hence thesis by A2;

    end;

    theorem :: LIMFUNC1:57

    f1 is divergent_in-infty_to+infty & (for r holds ex g st g < r & g in ( dom (f1 (#) f2))) & (ex r, r1 st 0 < r & for g st g in (( dom f2) /\ ( left_open_halfline r1)) holds r <= (f2 . g)) implies (f1 (#) f2) is divergent_in-infty_to+infty

    proof

      assume that

       A1: f1 is divergent_in-infty_to+infty and

       A2: for r holds ex g st g < r & g in ( dom (f1 (#) f2));

      given r2, r1 such that

       A3: 0 < r2 and

       A4: for g st g in (( dom f2) /\ ( left_open_halfline r1)) holds r2 <= (f2 . g);

      now

        let seq;

        assume that

         A5: seq is divergent_to-infty and

         A6: ( rng seq) c= ( dom (f1 (#) f2));

        consider k such that

         A7: for n st k <= n holds (seq . n) < r1 by A5;

        

         A8: ( rng (seq ^\ k)) c= ( rng seq) by VALUED_0: 21;

        

         A9: ( rng seq) c= ( dom f2) by A6, Lm3;

        then

         A10: ( rng (seq ^\ k)) c= ( dom f2) by A8;

         A11:

        now

          thus 0 < r2 by A3;

          let n;

          

           A12: n in NAT by ORDINAL1:def 12;

          (seq . (n + k)) < r1 by A7, NAT_1: 12;

          then ((seq ^\ k) . n) < r1 by NAT_1:def 3;

          then ((seq ^\ k) . n) in { g2 : g2 < r1 };

          then ((seq ^\ k) . n) in ( rng (seq ^\ k)) & ((seq ^\ k) . n) in ( left_open_halfline r1) by VALUED_0: 28, XXREAL_1: 229;

          then ((seq ^\ k) . n) in (( dom f2) /\ ( left_open_halfline r1)) by A10, XBOOLE_0:def 4;

          then r2 <= (f2 . ((seq ^\ k) . n)) by A4;

          hence r2 <= ((f2 /* (seq ^\ k)) . n) by A9, A8, FUNCT_2: 108, XBOOLE_1: 1, A12;

        end;

        ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by A6, Lm3;

        then ( rng (seq ^\ k)) c= (( dom f1) /\ ( dom f2)) by A6, A8;

        

        then

         A13: ((f1 /* (seq ^\ k)) (#) (f2 /* (seq ^\ k))) = ((f1 (#) f2) /* (seq ^\ k)) by RFUNCT_2: 8

        .= (((f1 (#) f2) /* seq) ^\ k) by A6, VALUED_0: 27;

        ( rng seq) c= ( dom f1) by A6, Lm3;

        then

         A14: ( rng (seq ^\ k)) c= ( dom f1) by A8;

        (seq ^\ k) is divergent_to-infty by A5, Th27;

        then (f1 /* (seq ^\ k)) is divergent_to+infty by A1, A14;

        then ((f1 /* (seq ^\ k)) (#) (f2 /* (seq ^\ k))) is divergent_to+infty by A11, Th22;

        hence ((f1 (#) f2) /* seq) is divergent_to+infty by A13, Th7;

      end;

      hence thesis by A2;

    end;

    theorem :: LIMFUNC1:58

    (f is divergent_in+infty_to+infty & r > 0 implies (r (#) f) is divergent_in+infty_to+infty) & (f is divergent_in+infty_to+infty & r < 0 implies (r (#) f) is divergent_in+infty_to-infty) & (f is divergent_in+infty_to-infty & r > 0 implies (r (#) f) is divergent_in+infty_to-infty) & (f is divergent_in+infty_to-infty & r < 0 implies (r (#) f) is divergent_in+infty_to+infty)

    proof

      thus f is divergent_in+infty_to+infty & r > 0 implies (r (#) f) is divergent_in+infty_to+infty

      proof

        assume that

         A1: f is divergent_in+infty_to+infty and

         A2: r > 0 ;

         A3:

        now

          let seq;

          assume that

           A4: seq is divergent_to+infty and

           A5: ( rng seq) c= ( dom (r (#) f));

          

           A6: ( rng seq) c= ( dom f) by A5, VALUED_1:def 5;

          then (f /* seq) is divergent_to+infty by A1, A4;

          then (r (#) (f /* seq)) is divergent_to+infty by A2, Th13;

          hence ((r (#) f) /* seq) is divergent_to+infty by A6, RFUNCT_2: 9;

        end;

        now

          let r1;

          consider g such that

           A7: r1 < g & g in ( dom f) by A1;

          take g;

          thus r1 < g & g in ( dom (r (#) f)) by A7, VALUED_1:def 5;

        end;

        hence thesis by A3;

      end;

      thus f is divergent_in+infty_to+infty & r < 0 implies (r (#) f) is divergent_in+infty_to-infty

      proof

        assume that

         A8: f is divergent_in+infty_to+infty and

         A9: r < 0 ;

         A10:

        now

          let seq;

          assume that

           A11: seq is divergent_to+infty and

           A12: ( rng seq) c= ( dom (r (#) f));

          

           A13: ( rng seq) c= ( dom f) by A12, VALUED_1:def 5;

          then (f /* seq) is divergent_to+infty by A8, A11;

          then (r (#) (f /* seq)) is divergent_to-infty by A9, Th13;

          hence ((r (#) f) /* seq) is divergent_to-infty by A13, RFUNCT_2: 9;

        end;

        now

          let r1;

          consider g such that

           A14: r1 < g & g in ( dom f) by A8;

          take g;

          thus r1 < g & g in ( dom (r (#) f)) by A14, VALUED_1:def 5;

        end;

        hence thesis by A10;

      end;

      thus f is divergent_in+infty_to-infty & r > 0 implies (r (#) f) is divergent_in+infty_to-infty

      proof

        assume that

         A15: f is divergent_in+infty_to-infty and

         A16: r > 0 ;

         A17:

        now

          let seq;

          assume that

           A18: seq is divergent_to+infty and

           A19: ( rng seq) c= ( dom (r (#) f));

          

           A20: ( rng seq) c= ( dom f) by A19, VALUED_1:def 5;

          then (f /* seq) is divergent_to-infty by A15, A18;

          then (r (#) (f /* seq)) is divergent_to-infty by A16, Th14;

          hence ((r (#) f) /* seq) is divergent_to-infty by A20, RFUNCT_2: 9;

        end;

        now

          let r1;

          consider g such that

           A21: r1 < g & g in ( dom f) by A15;

          take g;

          thus r1 < g & g in ( dom (r (#) f)) by A21, VALUED_1:def 5;

        end;

        hence thesis by A17;

      end;

      assume that

       A22: f is divergent_in+infty_to-infty and

       A23: r < 0 ;

       A24:

      now

        let seq;

        assume that

         A25: seq is divergent_to+infty and

         A26: ( rng seq) c= ( dom (r (#) f));

        

         A27: ( rng seq) c= ( dom f) by A26, VALUED_1:def 5;

        then (f /* seq) is divergent_to-infty by A22, A25;

        then (r (#) (f /* seq)) is divergent_to+infty by A23, Th14;

        hence ((r (#) f) /* seq) is divergent_to+infty by A27, RFUNCT_2: 9;

      end;

      now

        let r1;

        consider g such that

         A28: r1 < g & g in ( dom f) by A22;

        take g;

        thus r1 < g & g in ( dom (r (#) f)) by A28, VALUED_1:def 5;

      end;

      hence thesis by A24;

    end;

    theorem :: LIMFUNC1:59

    (f is divergent_in-infty_to+infty & r > 0 implies (r (#) f) is divergent_in-infty_to+infty) & (f is divergent_in-infty_to+infty & r < 0 implies (r (#) f) is divergent_in-infty_to-infty) & (f is divergent_in-infty_to-infty & r > 0 implies (r (#) f) is divergent_in-infty_to-infty) & (f is divergent_in-infty_to-infty & r < 0 implies (r (#) f) is divergent_in-infty_to+infty)

    proof

      thus f is divergent_in-infty_to+infty & r > 0 implies (r (#) f) is divergent_in-infty_to+infty

      proof

        assume that

         A1: f is divergent_in-infty_to+infty and

         A2: r > 0 ;

         A3:

        now

          let seq;

          assume that

           A4: seq is divergent_to-infty and

           A5: ( rng seq) c= ( dom (r (#) f));

          

           A6: ( rng seq) c= ( dom f) by A5, VALUED_1:def 5;

          then (f /* seq) is divergent_to+infty by A1, A4;

          then (r (#) (f /* seq)) is divergent_to+infty by A2, Th13;

          hence ((r (#) f) /* seq) is divergent_to+infty by A6, RFUNCT_2: 9;

        end;

        now

          let r1;

          consider g such that

           A7: g < r1 & g in ( dom f) by A1;

          take g;

          thus g < r1 & g in ( dom (r (#) f)) by A7, VALUED_1:def 5;

        end;

        hence thesis by A3;

      end;

      thus f is divergent_in-infty_to+infty & r < 0 implies (r (#) f) is divergent_in-infty_to-infty

      proof

        assume that

         A8: f is divergent_in-infty_to+infty and

         A9: r < 0 ;

         A10:

        now

          let seq;

          assume that

           A11: seq is divergent_to-infty and

           A12: ( rng seq) c= ( dom (r (#) f));

          

           A13: ( rng seq) c= ( dom f) by A12, VALUED_1:def 5;

          then (f /* seq) is divergent_to+infty by A8, A11;

          then (r (#) (f /* seq)) is divergent_to-infty by A9, Th13;

          hence ((r (#) f) /* seq) is divergent_to-infty by A13, RFUNCT_2: 9;

        end;

        now

          let r1;

          consider g such that

           A14: g < r1 & g in ( dom f) by A8;

          take g;

          thus g < r1 & g in ( dom (r (#) f)) by A14, VALUED_1:def 5;

        end;

        hence thesis by A10;

      end;

      thus f is divergent_in-infty_to-infty & r > 0 implies (r (#) f) is divergent_in-infty_to-infty

      proof

        assume that

         A15: f is divergent_in-infty_to-infty and

         A16: r > 0 ;

         A17:

        now

          let seq;

          assume that

           A18: seq is divergent_to-infty and

           A19: ( rng seq) c= ( dom (r (#) f));

          

           A20: ( rng seq) c= ( dom f) by A19, VALUED_1:def 5;

          then (f /* seq) is divergent_to-infty by A15, A18;

          then (r (#) (f /* seq)) is divergent_to-infty by A16, Th14;

          hence ((r (#) f) /* seq) is divergent_to-infty by A20, RFUNCT_2: 9;

        end;

        now

          let r1;

          consider g such that

           A21: g < r1 & g in ( dom f) by A15;

          take g;

          thus g < r1 & g in ( dom (r (#) f)) by A21, VALUED_1:def 5;

        end;

        hence thesis by A17;

      end;

      assume that

       A22: f is divergent_in-infty_to-infty and

       A23: r < 0 ;

       A24:

      now

        let seq;

        assume that

         A25: seq is divergent_to-infty and

         A26: ( rng seq) c= ( dom (r (#) f));

        

         A27: ( rng seq) c= ( dom f) by A26, VALUED_1:def 5;

        then (f /* seq) is divergent_to-infty by A22, A25;

        then (r (#) (f /* seq)) is divergent_to+infty by A23, Th14;

        hence ((r (#) f) /* seq) is divergent_to+infty by A27, RFUNCT_2: 9;

      end;

      now

        let r1;

        consider g such that

         A28: g < r1 & g in ( dom f) by A22;

        take g;

        thus g < r1 & g in ( dom (r (#) f)) by A28, VALUED_1:def 5;

      end;

      hence thesis by A24;

    end;

    theorem :: LIMFUNC1:60

    (f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty) implies ( abs f) is divergent_in+infty_to+infty

    proof

      assume

       A1: f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty;

      now

        per cases by A1;

          suppose

           A2: f is divergent_in+infty_to+infty;

           A3:

          now

            let seq;

            assume that

             A4: seq is divergent_to+infty and

             A5: ( rng seq) c= ( dom ( abs f));

            

             A6: ( rng seq) c= ( dom f) by A5, VALUED_1:def 11;

            then (f /* seq) is divergent_to+infty by A2, A4;

            then |.(f /* seq).| is divergent_to+infty by Th25;

            hence (( abs f) /* seq) is divergent_to+infty by A6, RFUNCT_2: 10;

          end;

          now

            let r;

            consider g such that

             A7: r < g & g in ( dom f) by A2;

            take g;

            thus r < g & g in ( dom ( abs f)) by A7, VALUED_1:def 11;

          end;

          hence thesis by A3;

        end;

          suppose

           A8: f is divergent_in+infty_to-infty;

           A9:

          now

            let seq;

            assume that

             A10: seq is divergent_to+infty and

             A11: ( rng seq) c= ( dom ( abs f));

            

             A12: ( rng seq) c= ( dom f) by A11, VALUED_1:def 11;

            then (f /* seq) is divergent_to-infty by A8, A10;

            then |.(f /* seq).| is divergent_to+infty by Th25;

            hence (( abs f) /* seq) is divergent_to+infty by A12, RFUNCT_2: 10;

          end;

          now

            let r;

            consider g such that

             A13: r < g & g in ( dom f) by A8;

            take g;

            thus r < g & g in ( dom ( abs f)) by A13, VALUED_1:def 11;

          end;

          hence thesis by A9;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC1:61

    (f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty) implies ( abs f) is divergent_in-infty_to+infty

    proof

      assume

       A1: f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty;

      now

        per cases by A1;

          suppose

           A2: f is divergent_in-infty_to+infty;

           A3:

          now

            let seq;

            assume that

             A4: seq is divergent_to-infty and

             A5: ( rng seq) c= ( dom ( abs f));

            

             A6: ( rng seq) c= ( dom f) by A5, VALUED_1:def 11;

            then (f /* seq) is divergent_to+infty by A2, A4;

            then ( abs (f /* seq)) is divergent_to+infty by Th25;

            hence (( abs f) /* seq) is divergent_to+infty by A6, RFUNCT_2: 10;

          end;

          now

            let r;

            consider g such that

             A7: g < r & g in ( dom f) by A2;

            take g;

            thus g < r & g in ( dom ( abs f)) by A7, VALUED_1:def 11;

          end;

          hence thesis by A3;

        end;

          suppose

           A8: f is divergent_in-infty_to-infty;

           A9:

          now

            let seq;

            assume that

             A10: seq is divergent_to-infty and

             A11: ( rng seq) c= ( dom ( abs f));

            

             A12: ( rng seq) c= ( dom f) by A11, VALUED_1:def 11;

            then (f /* seq) is divergent_to-infty by A8, A10;

            then ( abs (f /* seq)) is divergent_to+infty by Th25;

            hence (( abs f) /* seq) is divergent_to+infty by A12, RFUNCT_2: 10;

          end;

          now

            let r;

            consider g such that

             A13: g < r & g in ( dom f) by A8;

            take g;

            thus g < r & g in ( dom ( abs f)) by A13, VALUED_1:def 11;

          end;

          hence thesis by A9;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC1:62

    

     Th62: (ex r st (f | ( right_open_halfline r)) is non-decreasing & not (f | ( right_open_halfline r)) is bounded_above) & (for r holds ex g st r < g & g in ( dom f)) implies f is divergent_in+infty_to+infty

    proof

      given r1 such that

       A1: (f | ( right_open_halfline r1)) is non-decreasing and

       A2: not (f | ( right_open_halfline r1)) is bounded_above;

       A3:

      now

        let seq such that

         A4: seq is divergent_to+infty and

         A5: ( rng seq) c= ( dom f);

        now

          let r;

          consider g1 be object such that

           A6: g1 in (( right_open_halfline r1) /\ ( dom f)) and

           A7: r < (f . g1) by A2, RFUNCT_1: 70;

          reconsider g1 as Real by A6;

          consider n such that

           A8: for m st n <= m holds ( |.g1.| + |.r1.|) < (seq . m) by A4;

          take n;

          let m;

          

           A9: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then

           A10: ( |.g1.| + |.r1.|) < (seq . m) by A8;

          r1 <= |.r1.| & 0 <= |.g1.| by ABSVALUE: 4, COMPLEX1: 46;

          then ( 0 + r1) <= ( |.g1.| + |.r1.|) by XREAL_1: 7;

          then r1 < (seq . m) by A10, XXREAL_0: 2;

          then (seq . m) in { g2 : r1 < g2 };

          then (seq . m) in ( rng seq) & (seq . m) in ( right_open_halfline r1) by VALUED_0: 28, XXREAL_1: 230;

          then

           A11: (seq . m) in (( right_open_halfline r1) /\ ( dom f)) by A5, XBOOLE_0:def 4;

          g1 <= |.g1.| & 0 <= |.r1.| by ABSVALUE: 4, COMPLEX1: 46;

          then (g1 + 0 ) <= ( |.g1.| + |.r1.|) by XREAL_1: 7;

          then g1 < (seq . m) by A10, XXREAL_0: 2;

          then (f . g1) <= (f . (seq . m)) by A1, A6, A11, RFUNCT_2: 22;

          then r < (f . (seq . m)) by A7, XXREAL_0: 2;

          hence r < ((f /* seq) . m) by A5, FUNCT_2: 108, A9;

        end;

        hence (f /* seq) is divergent_to+infty;

      end;

      assume for r holds ex g st r < g & g in ( dom f);

      hence thesis by A3;

    end;

    theorem :: LIMFUNC1:63

    (ex r st (f | ( right_open_halfline r)) is increasing & not (f | ( right_open_halfline r)) is bounded_above) & (for r holds ex g st r < g & g in ( dom f)) implies f is divergent_in+infty_to+infty by Th62;

    theorem :: LIMFUNC1:64

    

     Th64: (ex r st (f | ( right_open_halfline r)) is non-increasing & not (f | ( right_open_halfline r)) is bounded_below) & (for r holds ex g st r < g & g in ( dom f)) implies f is divergent_in+infty_to-infty

    proof

      given r1 such that

       A1: (f | ( right_open_halfline r1)) is non-increasing and

       A2: not (f | ( right_open_halfline r1)) is bounded_below;

       A3:

      now

        let seq such that

         A4: seq is divergent_to+infty and

         A5: ( rng seq) c= ( dom f);

        now

          let r;

          consider g1 be object such that

           A6: g1 in (( right_open_halfline r1) /\ ( dom f)) and

           A7: (f . g1) < r by A2, RFUNCT_1: 71;

          reconsider g1 as Real by A6;

          consider n such that

           A8: for m st n <= m holds ( |.g1.| + |.r1.|) < (seq . m) by A4;

          take n;

          let m;

          

           A9: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then

           A10: ( |.g1.| + |.r1.|) < (seq . m) by A8;

          r1 <= |.r1.| & 0 <= |.g1.| by ABSVALUE: 4, COMPLEX1: 46;

          then ( 0 + r1) <= ( |.g1.| + |.r1.|) by XREAL_1: 7;

          then r1 < (seq . m) by A10, XXREAL_0: 2;

          then (seq . m) in { g2 : r1 < g2 };

          then (seq . m) in ( rng seq) & (seq . m) in ( right_open_halfline r1) by VALUED_0: 28, XXREAL_1: 230;

          then

           A11: (seq . m) in (( right_open_halfline r1) /\ ( dom f)) by A5, XBOOLE_0:def 4;

          g1 <= |.g1.| & 0 <= |.r1.| by ABSVALUE: 4, COMPLEX1: 46;

          then (g1 + 0 ) <= ( |.g1.| + |.r1.|) by XREAL_1: 7;

          then g1 < (seq . m) by A10, XXREAL_0: 2;

          then (f . (seq . m)) <= (f . g1) by A1, A6, A11, RFUNCT_2: 23;

          then (f . (seq . m)) < r by A7, XXREAL_0: 2;

          hence ((f /* seq) . m) < r by A5, FUNCT_2: 108, A9;

        end;

        hence (f /* seq) is divergent_to-infty;

      end;

      assume for r holds ex g st r < g & g in ( dom f);

      hence thesis by A3;

    end;

    theorem :: LIMFUNC1:65

    (ex r st (f | ( right_open_halfline r)) is decreasing & not (f | ( right_open_halfline r)) is bounded_below) & (for r holds ex g st r < g & g in ( dom f)) implies f is divergent_in+infty_to-infty by Th64;

    theorem :: LIMFUNC1:66

    

     Th66: (ex r st (f | ( left_open_halfline r)) is non-increasing & not (f | ( left_open_halfline r)) is bounded_above) & (for r holds ex g st g < r & g in ( dom f)) implies f is divergent_in-infty_to+infty

    proof

      given r1 such that

       A1: (f | ( left_open_halfline r1)) is non-increasing and

       A2: not (f | ( left_open_halfline r1)) is bounded_above;

       A3:

      now

        let seq such that

         A4: seq is divergent_to-infty and

         A5: ( rng seq) c= ( dom f);

        now

          let r;

          consider g1 be object such that

           A6: g1 in (( left_open_halfline r1) /\ ( dom f)) and

           A7: r < (f . g1) by A2, RFUNCT_1: 70;

          reconsider g1 as Real by A6;

          consider n such that

           A8: for m st n <= m holds (seq . m) < (( - |.r1.|) - |.g1.|) by A4;

          take n;

          let m;

          

           A9: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then

           A10: (seq . m) < (( - |.r1.|) - |.g1.|) by A8;

          ( - |.r1.|) <= r1 & 0 <= |.g1.| by ABSVALUE: 4, COMPLEX1: 46;

          then (( - |.r1.|) - |.g1.|) <= (r1 - 0 ) by XREAL_1: 13;

          then (seq . m) < r1 by A10, XXREAL_0: 2;

          then (seq . m) in { g2 : g2 < r1 };

          then (seq . m) in ( rng seq) & (seq . m) in ( left_open_halfline r1) by VALUED_0: 28, XXREAL_1: 229;

          then

           A11: (seq . m) in (( left_open_halfline r1) /\ ( dom f)) by A5, XBOOLE_0:def 4;

          ( - |.g1.|) <= g1 & 0 <= |.r1.| by ABSVALUE: 4, COMPLEX1: 46;

          then (( - |.g1.|) - |.r1.|) <= (g1 - 0 ) by XREAL_1: 13;

          then (seq . m) < g1 by A10, XXREAL_0: 2;

          then (f . g1) <= (f . (seq . m)) by A1, A6, A11, RFUNCT_2: 23;

          then r < (f . (seq . m)) by A7, XXREAL_0: 2;

          hence r < ((f /* seq) . m) by A5, FUNCT_2: 108, A9;

        end;

        hence (f /* seq) is divergent_to+infty;

      end;

      assume for r holds ex g st g < r & g in ( dom f);

      hence thesis by A3;

    end;

    theorem :: LIMFUNC1:67

    (ex r st (f | ( left_open_halfline r)) is decreasing & not (f | ( left_open_halfline r)) is bounded_above) & (for r holds ex g st g < r & g in ( dom f)) implies f is divergent_in-infty_to+infty by Th66;

    theorem :: LIMFUNC1:68

    

     Th68: (ex r st (f | ( left_open_halfline r)) is non-decreasing & not (f | ( left_open_halfline r)) is bounded_below) & (for r holds ex g st g < r & g in ( dom f)) implies f is divergent_in-infty_to-infty

    proof

      given r1 such that

       A1: (f | ( left_open_halfline r1)) is non-decreasing and

       A2: not (f | ( left_open_halfline r1)) is bounded_below;

       A3:

      now

        let seq such that

         A4: seq is divergent_to-infty and

         A5: ( rng seq) c= ( dom f);

        now

          let r;

          consider g1 be object such that

           A6: g1 in (( left_open_halfline r1) /\ ( dom f)) and

           A7: (f . g1) < r by A2, RFUNCT_1: 71;

          reconsider g1 as Real by A6;

          consider n such that

           A8: for m st n <= m holds (seq . m) < (( - |.r1.|) - |.g1.|) by A4;

          take n;

          let m;

          

           A9: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then

           A10: (seq . m) < (( - |.r1.|) - |.g1.|) by A8;

          ( - |.r1.|) <= r1 & 0 <= |.g1.| by ABSVALUE: 4, COMPLEX1: 46;

          then (( - |.r1.|) - |.g1.|) <= (r1 - 0 ) by XREAL_1: 13;

          then (seq . m) < r1 by A10, XXREAL_0: 2;

          then (seq . m) in { g2 : g2 < r1 };

          then (seq . m) in ( rng seq) & (seq . m) in ( left_open_halfline r1) by VALUED_0: 28, XXREAL_1: 229;

          then

           A11: (seq . m) in (( left_open_halfline r1) /\ ( dom f)) by A5, XBOOLE_0:def 4;

          ( - |.g1.|) <= g1 & 0 <= |.r1.| by ABSVALUE: 4, COMPLEX1: 46;

          then (( - |.g1.|) - |.r1.|) <= (g1 - 0 ) by XREAL_1: 13;

          then (seq . m) < g1 by A10, XXREAL_0: 2;

          then (f . (seq . m)) <= (f . g1) by A1, A6, A11, RFUNCT_2: 22;

          then (f . (seq . m)) < r by A7, XXREAL_0: 2;

          hence ((f /* seq) . m) < r by A5, FUNCT_2: 108, A9;

        end;

        hence (f /* seq) is divergent_to-infty;

      end;

      assume for r holds ex g st g < r & g in ( dom f);

      hence thesis by A3;

    end;

    theorem :: LIMFUNC1:69

    (ex r st (f | ( left_open_halfline r)) is increasing & not (f | ( left_open_halfline r)) is bounded_below) & (for r holds ex g st g < r & g in ( dom f)) implies f is divergent_in-infty_to-infty by Th68;

    theorem :: LIMFUNC1:70

    

     Th70: f1 is divergent_in+infty_to+infty & (for r holds ex g st r < g & g in ( dom f)) & (ex r st (( dom f) /\ ( right_open_halfline r)) c= (( dom f1) /\ ( right_open_halfline r)) & for g st g in (( dom f) /\ ( right_open_halfline r)) holds (f1 . g) <= (f . g)) implies f is divergent_in+infty_to+infty

    proof

      assume that

       A1: f1 is divergent_in+infty_to+infty and

       A2: for r holds ex g st r < g & g in ( dom f);

      given r1 such that

       A3: (( dom f) /\ ( right_open_halfline r1)) c= (( dom f1) /\ ( right_open_halfline r1)) and

       A4: for g st g in (( dom f) /\ ( right_open_halfline r1)) holds (f1 . g) <= (f . g);

      now

        let seq;

        assume that

         A5: seq is divergent_to+infty and

         A6: ( rng seq) c= ( dom f);

        consider k such that

         A7: for n st k <= n holds r1 < (seq . n) by A5;

        now

          let x be object;

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

          then

          consider n be Element of NAT such that

           A8: ((seq ^\ k) . n) = x by FUNCT_2: 113;

          r1 < (seq . (n + k)) by A7, NAT_1: 12;

          then r1 < ((seq ^\ k) . n) by NAT_1:def 3;

          then x in { g2 : r1 < g2 } by A8;

          hence x in ( right_open_halfline r1) by XXREAL_1: 230;

        end;

        then

         A9: ( rng (seq ^\ k)) c= ( right_open_halfline r1);

        

         A10: ( rng (seq ^\ k)) c= ( rng seq) by VALUED_0: 21;

        then ( rng (seq ^\ k)) c= ( dom f) by A6;

        then

         A11: ( rng (seq ^\ k)) c= (( dom f) /\ ( right_open_halfline r1)) by A9, XBOOLE_1: 19;

        then

         A12: ( rng (seq ^\ k)) c= (( dom f1) /\ ( right_open_halfline r1)) by A3;

        

         A13: (( dom f1) /\ ( right_open_halfline r1)) c= ( dom f1) by XBOOLE_1: 17;

         A14:

        now

          let n;

          

           A15: n in NAT by ORDINAL1:def 12;

          ((seq ^\ k) . n) in ( rng (seq ^\ k)) by VALUED_0: 28;

          then (f1 . ((seq ^\ k) . n)) <= (f . ((seq ^\ k) . n)) by A4, A11;

          then ((f1 /* (seq ^\ k)) . n) <= (f . ((seq ^\ k) . n)) by A12, A13, FUNCT_2: 108, XBOOLE_1: 1, A15;

          hence ((f1 /* (seq ^\ k)) . n) <= ((f /* (seq ^\ k)) . n) by A6, A10, FUNCT_2: 108, XBOOLE_1: 1, A15;

        end;

        

         A16: (seq ^\ k) is divergent_to+infty by A5, Th26;

        ( rng (seq ^\ k)) c= ( dom f1) by A12, A13;

        then (f1 /* (seq ^\ k)) is divergent_to+infty by A1, A16;

        then

         A17: (f /* (seq ^\ k)) is divergent_to+infty by A14, Th42;

        (f /* (seq ^\ k)) = ((f /* seq) ^\ k) by A6, VALUED_0: 27;

        hence (f /* seq) is divergent_to+infty by A17, Th7;

      end;

      hence thesis by A2;

    end;

    theorem :: LIMFUNC1:71

    

     Th71: f1 is divergent_in+infty_to-infty & (for r holds ex g st r < g & g in ( dom f)) & (ex r st (( dom f) /\ ( right_open_halfline r)) c= (( dom f1) /\ ( right_open_halfline r)) & for g st g in (( dom f) /\ ( right_open_halfline r)) holds (f . g) <= (f1 . g)) implies f is divergent_in+infty_to-infty

    proof

      assume that

       A1: f1 is divergent_in+infty_to-infty and

       A2: for r holds ex g st r < g & g in ( dom f);

      given r1 such that

       A3: (( dom f) /\ ( right_open_halfline r1)) c= (( dom f1) /\ ( right_open_halfline r1)) and

       A4: for g st g in (( dom f) /\ ( right_open_halfline r1)) holds (f . g) <= (f1 . g);

      now

        let seq;

        assume that

         A5: seq is divergent_to+infty and

         A6: ( rng seq) c= ( dom f);

        consider k such that

         A7: for n st k <= n holds r1 < (seq . n) by A5;

        now

          let x be object;

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

          then

          consider n be Element of NAT such that

           A8: ((seq ^\ k) . n) = x by FUNCT_2: 113;

          r1 < (seq . (n + k)) by A7, NAT_1: 12;

          then r1 < ((seq ^\ k) . n) by NAT_1:def 3;

          then x in { g2 : r1 < g2 } by A8;

          hence x in ( right_open_halfline r1) by XXREAL_1: 230;

        end;

        then

         A9: ( rng (seq ^\ k)) c= ( right_open_halfline r1);

        

         A10: ( rng (seq ^\ k)) c= ( rng seq) by VALUED_0: 21;

        then ( rng (seq ^\ k)) c= ( dom f) by A6;

        then

         A11: ( rng (seq ^\ k)) c= (( dom f) /\ ( right_open_halfline r1)) by A9, XBOOLE_1: 19;

        then

         A12: ( rng (seq ^\ k)) c= (( dom f1) /\ ( right_open_halfline r1)) by A3;

        

         A13: (( dom f1) /\ ( right_open_halfline r1)) c= ( dom f1) by XBOOLE_1: 17;

         A14:

        now

          let n;

          

           A15: n in NAT by ORDINAL1:def 12;

          ((seq ^\ k) . n) in ( rng (seq ^\ k)) by VALUED_0: 28;

          then (f . ((seq ^\ k) . n)) <= (f1 . ((seq ^\ k) . n)) by A4, A11;

          then ((f /* (seq ^\ k)) . n) <= (f1 . ((seq ^\ k) . n)) by A6, A10, FUNCT_2: 108, XBOOLE_1: 1, A15;

          hence ((f /* (seq ^\ k)) . n) <= ((f1 /* (seq ^\ k)) . n) by A12, A13, FUNCT_2: 108, XBOOLE_1: 1, A15;

        end;

        

         A16: (seq ^\ k) is divergent_to+infty by A5, Th26;

        ( rng (seq ^\ k)) c= ( dom f1) by A12, A13;

        then (f1 /* (seq ^\ k)) is divergent_to-infty by A1, A16;

        then

         A17: (f /* (seq ^\ k)) is divergent_to-infty by A14, Th43;

        (f /* (seq ^\ k)) = ((f /* seq) ^\ k) by A6, VALUED_0: 27;

        hence (f /* seq) is divergent_to-infty by A17, Th7;

      end;

      hence thesis by A2;

    end;

    theorem :: LIMFUNC1:72

    

     Th72: f1 is divergent_in-infty_to+infty & (for r holds ex g st g < r & g in ( dom f)) & (ex r st (( dom f) /\ ( left_open_halfline r)) c= (( dom f1) /\ ( left_open_halfline r)) & for g st g in (( dom f) /\ ( left_open_halfline r)) holds (f1 . g) <= (f . g)) implies f is divergent_in-infty_to+infty

    proof

      assume that

       A1: f1 is divergent_in-infty_to+infty and

       A2: for r holds ex g st g < r & g in ( dom f);

      given r1 such that

       A3: (( dom f) /\ ( left_open_halfline r1)) c= (( dom f1) /\ ( left_open_halfline r1)) and

       A4: for g st g in (( dom f) /\ ( left_open_halfline r1)) holds (f1 . g) <= (f . g);

      now

        let seq;

        assume that

         A5: seq is divergent_to-infty and

         A6: ( rng seq) c= ( dom f);

        consider k such that

         A7: for n st k <= n holds (seq . n) < r1 by A5;

        now

          let x be object;

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

          then

          consider n be Element of NAT such that

           A8: ((seq ^\ k) . n) = x by FUNCT_2: 113;

          (seq . (n + k)) < r1 by A7, NAT_1: 12;

          then ((seq ^\ k) . n) < r1 by NAT_1:def 3;

          then x in { g2 : g2 < r1 } by A8;

          hence x in ( left_open_halfline r1) by XXREAL_1: 229;

        end;

        then

         A9: ( rng (seq ^\ k)) c= ( left_open_halfline r1);

        

         A10: ( rng (seq ^\ k)) c= ( rng seq) by VALUED_0: 21;

        then ( rng (seq ^\ k)) c= ( dom f) by A6;

        then

         A11: ( rng (seq ^\ k)) c= (( dom f) /\ ( left_open_halfline r1)) by A9, XBOOLE_1: 19;

        then

         A12: ( rng (seq ^\ k)) c= (( dom f1) /\ ( left_open_halfline r1)) by A3;

        

         A13: (( dom f1) /\ ( left_open_halfline r1)) c= ( dom f1) by XBOOLE_1: 17;

         A14:

        now

          let n;

          

           A15: n in NAT by ORDINAL1:def 12;

          ((seq ^\ k) . n) in ( rng (seq ^\ k)) by VALUED_0: 28;

          then (f1 . ((seq ^\ k) . n)) <= (f . ((seq ^\ k) . n)) by A4, A11;

          then ((f1 /* (seq ^\ k)) . n) <= (f . ((seq ^\ k) . n)) by A12, A13, FUNCT_2: 108, XBOOLE_1: 1, A15;

          hence ((f1 /* (seq ^\ k)) . n) <= ((f /* (seq ^\ k)) . n) by A6, A10, FUNCT_2: 108, XBOOLE_1: 1, A15;

        end;

        

         A16: (seq ^\ k) is divergent_to-infty by A5, Th27;

        ( rng (seq ^\ k)) c= ( dom f1) by A12, A13;

        then (f1 /* (seq ^\ k)) is divergent_to+infty by A1, A16;

        then

         A17: (f /* (seq ^\ k)) is divergent_to+infty by A14, Th42;

        (f /* (seq ^\ k)) = ((f /* seq) ^\ k) by A6, VALUED_0: 27;

        hence (f /* seq) is divergent_to+infty by A17, Th7;

      end;

      hence thesis by A2;

    end;

    theorem :: LIMFUNC1:73

    

     Th73: f1 is divergent_in-infty_to-infty & (for r holds ex g st g < r & g in ( dom f)) & (ex r st (( dom f) /\ ( left_open_halfline r)) c= (( dom f1) /\ ( left_open_halfline r)) & for g st g in (( dom f) /\ ( left_open_halfline r)) holds (f . g) <= (f1 . g)) implies f is divergent_in-infty_to-infty

    proof

      assume that

       A1: f1 is divergent_in-infty_to-infty and

       A2: for r holds ex g st g < r & g in ( dom f);

      given r1 such that

       A3: (( dom f) /\ ( left_open_halfline r1)) c= (( dom f1) /\ ( left_open_halfline r1)) and

       A4: for g st g in (( dom f) /\ ( left_open_halfline r1)) holds (f . g) <= (f1 . g);

      now

        let seq;

        assume that

         A5: seq is divergent_to-infty and

         A6: ( rng seq) c= ( dom f);

        consider k such that

         A7: for n st k <= n holds (seq . n) < r1 by A5;

        now

          let x be object;

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

          then

          consider n be Element of NAT such that

           A8: ((seq ^\ k) . n) = x by FUNCT_2: 113;

          (seq . (n + k)) < r1 by A7, NAT_1: 12;

          then ((seq ^\ k) . n) < r1 by NAT_1:def 3;

          then x in { g2 : g2 < r1 } by A8;

          hence x in ( left_open_halfline r1) by XXREAL_1: 229;

        end;

        then

         A9: ( rng (seq ^\ k)) c= ( left_open_halfline r1);

        

         A10: ( rng (seq ^\ k)) c= ( rng seq) by VALUED_0: 21;

        then ( rng (seq ^\ k)) c= ( dom f) by A6;

        then

         A11: ( rng (seq ^\ k)) c= (( dom f) /\ ( left_open_halfline r1)) by A9, XBOOLE_1: 19;

        then

         A12: ( rng (seq ^\ k)) c= (( dom f1) /\ ( left_open_halfline r1)) by A3;

        

         A13: (( dom f1) /\ ( left_open_halfline r1)) c= ( dom f1) by XBOOLE_1: 17;

         A14:

        now

          let n;

          

           A15: n in NAT by ORDINAL1:def 12;

          ((seq ^\ k) . n) in ( rng (seq ^\ k)) by VALUED_0: 28;

          then (f . ((seq ^\ k) . n)) <= (f1 . ((seq ^\ k) . n)) by A4, A11;

          then ((f /* (seq ^\ k)) . n) <= (f1 . ((seq ^\ k) . n)) by A6, A10, FUNCT_2: 108, XBOOLE_1: 1, A15;

          hence ((f /* (seq ^\ k)) . n) <= ((f1 /* (seq ^\ k)) . n) by A12, A13, FUNCT_2: 108, XBOOLE_1: 1, A15;

        end;

        

         A16: (seq ^\ k) is divergent_to-infty by A5, Th27;

        ( rng (seq ^\ k)) c= ( dom f1) by A12, A13;

        then (f1 /* (seq ^\ k)) is divergent_to-infty by A1, A16;

        then

         A17: (f /* (seq ^\ k)) is divergent_to-infty by A14, Th43;

        (f /* (seq ^\ k)) = ((f /* seq) ^\ k) by A6, VALUED_0: 27;

        hence (f /* seq) is divergent_to-infty by A17, Th7;

      end;

      hence thesis by A2;

    end;

    theorem :: LIMFUNC1:74

    f1 is divergent_in+infty_to+infty & (ex r st ( right_open_halfline r) c= (( dom f) /\ ( dom f1)) & for g st g in ( right_open_halfline r) holds (f1 . g) <= (f . g)) implies f is divergent_in+infty_to+infty

    proof

      assume

       A1: f1 is divergent_in+infty_to+infty;

      given r1 such that

       A2: ( right_open_halfline r1) c= (( dom f) /\ ( dom f1)) and

       A3: for g st g in ( right_open_halfline r1) holds (f1 . g) <= (f . g);

       A4:

      now

        let r;

        consider g be Real such that

         A5: ( |.r.| + |.r1.|) < g by XREAL_1: 1;

        take g;

         0 <= |.r1.| & r <= |.r.| by ABSVALUE: 4, COMPLEX1: 46;

        then ( 0 + r) <= ( |.r.| + |.r1.|) by XREAL_1: 7;

        hence r < g by A5, XXREAL_0: 2;

         0 <= |.r.| & r1 <= |.r1.| by ABSVALUE: 4, COMPLEX1: 46;

        then ( 0 + r1) <= ( |.r.| + |.r1.|) by XREAL_1: 7;

        then r1 < g by A5, XXREAL_0: 2;

        then g in { g2 : r1 < g2 };

        then g in ( right_open_halfline r1) by XXREAL_1: 230;

        hence g in ( dom f) by A2, XBOOLE_0:def 4;

      end;

      now

        (( dom f) /\ ( dom f1)) c= ( dom f) by XBOOLE_1: 17;

        then

         A6: (( dom f) /\ ( right_open_halfline r1)) = ( right_open_halfline r1) by A2, XBOOLE_1: 1, XBOOLE_1: 28;

        (( dom f) /\ ( dom f1)) c= ( dom f1) by XBOOLE_1: 17;

        hence (( dom f) /\ ( right_open_halfline r1)) c= (( dom f1) /\ ( right_open_halfline r1)) by A2, A6, XBOOLE_1: 1, XBOOLE_1: 28;

        let g;

        assume g in (( dom f) /\ ( right_open_halfline r1));

        hence (f1 . g) <= (f . g) by A3, A6;

      end;

      hence thesis by A1, A4, Th70;

    end;

    theorem :: LIMFUNC1:75

    f1 is divergent_in+infty_to-infty & (ex r st ( right_open_halfline r) c= (( dom f) /\ ( dom f1)) & for g st g in ( right_open_halfline r) holds (f . g) <= (f1 . g)) implies f is divergent_in+infty_to-infty

    proof

      assume

       A1: f1 is divergent_in+infty_to-infty;

      given r1 such that

       A2: ( right_open_halfline r1) c= (( dom f) /\ ( dom f1)) and

       A3: for g st g in ( right_open_halfline r1) holds (f . g) <= (f1 . g);

       A4:

      now

        let r;

        consider g be Real such that

         A5: ( |.r.| + |.r1.|) < g by XREAL_1: 1;

        take g;

         0 <= |.r1.| & r <= |.r.| by ABSVALUE: 4, COMPLEX1: 46;

        then ( 0 + r) <= ( |.r.| + |.r1.|) by XREAL_1: 7;

        hence r < g by A5, XXREAL_0: 2;

         0 <= |.r.| & r1 <= |.r1.| by ABSVALUE: 4, COMPLEX1: 46;

        then ( 0 + r1) <= ( |.r.| + |.r1.|) by XREAL_1: 7;

        then r1 < g by A5, XXREAL_0: 2;

        then g in { g2 : r1 < g2 };

        then g in ( right_open_halfline r1) by XXREAL_1: 230;

        hence g in ( dom f) by A2, XBOOLE_0:def 4;

      end;

      now

        (( dom f) /\ ( dom f1)) c= ( dom f) by XBOOLE_1: 17;

        then

         A6: (( dom f) /\ ( right_open_halfline r1)) = ( right_open_halfline r1) by A2, XBOOLE_1: 1, XBOOLE_1: 28;

        (( dom f) /\ ( dom f1)) c= ( dom f1) by XBOOLE_1: 17;

        hence (( dom f) /\ ( right_open_halfline r1)) c= (( dom f1) /\ ( right_open_halfline r1)) by A2, A6, XBOOLE_1: 1, XBOOLE_1: 28;

        let g;

        assume g in (( dom f) /\ ( right_open_halfline r1));

        hence (f . g) <= (f1 . g) by A3, A6;

      end;

      hence thesis by A1, A4, Th71;

    end;

    theorem :: LIMFUNC1:76

    f1 is divergent_in-infty_to+infty & (ex r st ( left_open_halfline r) c= (( dom f) /\ ( dom f1)) & for g st g in ( left_open_halfline r) holds (f1 . g) <= (f . g)) implies f is divergent_in-infty_to+infty

    proof

      assume

       A1: f1 is divergent_in-infty_to+infty;

      given r1 such that

       A2: ( left_open_halfline r1) c= (( dom f) /\ ( dom f1)) and

       A3: for g st g in ( left_open_halfline r1) holds (f1 . g) <= (f . g);

       A4:

      now

        let r;

        consider g be Real such that

         A5: g < (( - |.r.|) - |.r1.|) by XREAL_1: 2;

        take g;

         0 <= |.r1.| & ( - |.r.|) <= r by ABSVALUE: 4, COMPLEX1: 46;

        then (( - |.r.|) - |.r1.|) <= (r - 0 ) by XREAL_1: 13;

        hence g < r by A5, XXREAL_0: 2;

         0 <= |.r.| & ( - |.r1.|) <= r1 by ABSVALUE: 4, COMPLEX1: 46;

        then (( - |.r1.|) - |.r.|) <= (r1 - 0 ) by XREAL_1: 13;

        then g < r1 by A5, XXREAL_0: 2;

        then g in { g2 : g2 < r1 };

        then g in ( left_open_halfline r1) by XXREAL_1: 229;

        hence g in ( dom f) by A2, XBOOLE_0:def 4;

      end;

      now

        (( dom f) /\ ( dom f1)) c= ( dom f) by XBOOLE_1: 17;

        then

         A6: (( dom f) /\ ( left_open_halfline r1)) = ( left_open_halfline r1) by A2, XBOOLE_1: 1, XBOOLE_1: 28;

        (( dom f) /\ ( dom f1)) c= ( dom f1) by XBOOLE_1: 17;

        hence (( dom f) /\ ( left_open_halfline r1)) c= (( dom f1) /\ ( left_open_halfline r1)) by A2, A6, XBOOLE_1: 1, XBOOLE_1: 28;

        let g;

        assume g in (( dom f) /\ ( left_open_halfline r1));

        hence (f1 . g) <= (f . g) by A3, A6;

      end;

      hence thesis by A1, A4, Th72;

    end;

    theorem :: LIMFUNC1:77

    f1 is divergent_in-infty_to-infty & (ex r st ( left_open_halfline r) c= (( dom f) /\ ( dom f1)) & for g st g in ( left_open_halfline r) holds (f . g) <= (f1 . g)) implies f is divergent_in-infty_to-infty

    proof

      assume

       A1: f1 is divergent_in-infty_to-infty;

      given r1 such that

       A2: ( left_open_halfline r1) c= (( dom f) /\ ( dom f1)) and

       A3: for g st g in ( left_open_halfline r1) holds (f . g) <= (f1 . g);

       A4:

      now

        let r;

        consider g be Real such that

         A5: g < (( - |.r.|) - |.r1.|) by XREAL_1: 2;

        take g;

         0 <= |.r1.| & ( - |.r.|) <= r by ABSVALUE: 4, COMPLEX1: 46;

        then (( - |.r.|) - |.r1.|) <= (r - 0 ) by XREAL_1: 13;

        hence g < r by A5, XXREAL_0: 2;

         0 <= |.r.| & ( - |.r1.|) <= r1 by ABSVALUE: 4, COMPLEX1: 46;

        then (( - |.r1.|) - |.r.|) <= (r1 - 0 ) by XREAL_1: 13;

        then g < r1 by A5, XXREAL_0: 2;

        then g in { g2 : g2 < r1 };

        then g in ( left_open_halfline r1) by XXREAL_1: 229;

        hence g in ( dom f) by A2, XBOOLE_0:def 4;

      end;

      now

        (( dom f) /\ ( dom f1)) c= ( dom f) by XBOOLE_1: 17;

        then

         A6: (( dom f) /\ ( left_open_halfline r1)) = ( left_open_halfline r1) by A2, XBOOLE_1: 1, XBOOLE_1: 28;

        (( dom f) /\ ( dom f1)) c= ( dom f1) by XBOOLE_1: 17;

        hence (( dom f) /\ ( left_open_halfline r1)) c= (( dom f1) /\ ( left_open_halfline r1)) by A2, A6, XBOOLE_1: 1, XBOOLE_1: 28;

        let g;

        assume g in (( dom f) /\ ( left_open_halfline r1));

        hence (f . g) <= (f1 . g) by A3, A6;

      end;

      hence thesis by A1, A4, Th73;

    end;

    definition

      let f;

      assume

       A1: f is convergent_in+infty;

      :: LIMFUNC1:def12

      func lim_in+infty f -> Real means

      : Def12: for seq st seq is divergent_to+infty & ( rng seq) c= ( dom f) holds (f /* seq) is convergent & ( lim (f /* seq)) = it ;

      existence by A1;

      uniqueness

      proof

        defpred X[ Nat, Real] means $1 < $2 & $2 in ( dom f);

        let g1,g2 be Real such that

         A2: for seq st seq is divergent_to+infty & ( rng seq) c= ( dom f) holds (f /* seq) is convergent & ( lim (f /* seq)) = g1 and

         A3: for seq st seq is divergent_to+infty & ( rng seq) c= ( dom f) holds (f /* seq) is convergent & ( lim (f /* seq)) = g2;

        

         A4: for n be Element of NAT holds ex r be Element of REAL st X[n, r]

        proof

          let n be Element of NAT ;

          consider r such that

           A5: X[n, r] by A1;

          reconsider r as Real;

           X[n, r] by A5;

          hence thesis;

        end;

        consider s2 be Real_Sequence such that

         A6: for n be Element of NAT holds X[n, (s2 . n)] from FUNCT_2:sch 3( A4);

        

         A7: ( rng s2) c= ( dom f)

        proof

          let x be Real;

          assume x in ( rng s2);

          then ex n be Element of NAT st x = (s2 . n) by FUNCT_2: 113;

          hence thesis by A6;

        end;

        now

          let n;

          

           A8: n in NAT by ORDINAL1:def 12;

          then n < (s2 . n) by A6;

          hence (s1 . n) <= (s2 . n) by FUNCT_1: 18, A8;

        end;

        then

         A9: s2 is divergent_to+infty by Lm5, Th20, Th42;

        then ( lim (f /* s2)) = g1 by A2, A7;

        hence thesis by A3, A9, A7;

      end;

    end

    definition

      let f;

      assume

       A1: f is convergent_in-infty;

      :: LIMFUNC1:def13

      func lim_in-infty f -> Real means

      : Def13: for seq st seq is divergent_to-infty & ( rng seq) c= ( dom f) holds (f /* seq) is convergent & ( lim (f /* seq)) = it ;

      existence by A1;

      uniqueness

      proof

        deffunc U( Nat) = ( - $1);

        defpred X[ Nat, Real] means $2 < ( - $1) & $2 in ( dom f);

        let g1,g2 be Real such that

         A2: for seq st seq is divergent_to-infty & ( rng seq) c= ( dom f) holds (f /* seq) is convergent & ( lim (f /* seq)) = g1 and

         A3: for seq st seq is divergent_to-infty & ( rng seq) c= ( dom f) holds (f /* seq) is convergent & ( lim (f /* seq)) = g2;

        consider s2 be Real_Sequence such that

         A4: for n holds (s2 . n) = U(n) from SEQ_1:sch 1;

        

         A5: for n be Element of NAT holds ex r be Element of REAL st X[n, r]

        proof

          let n be Element of NAT ;

          consider r such that

           A6: X[n, r] by A1;

          reconsider r as Real;

           X[n, r] by A6;

          hence thesis;

        end;

        consider s1 be Real_Sequence such that

         A7: for n be Element of NAT holds X[n, (s1 . n)] from FUNCT_2:sch 3( A5);

        

         A8: ( rng s1) c= ( dom f)

        proof

          let x be Real;

          assume x in ( rng s1);

          then ex n be Element of NAT st x = (s1 . n) by FUNCT_2: 113;

          hence thesis by A7;

        end;

        now

          let n;

          n in NAT by ORDINAL1:def 12;

          then (s1 . n) < ( - n) by A7;

          hence (s1 . n) <= (s2 . n) by A4;

        end;

        then

         A9: s1 is divergent_to-infty by A4, Th21, Th43;

        then ( lim (f /* s1)) = g1 by A2, A8;

        hence thesis by A3, A9, A8;

      end;

    end

    theorem :: LIMFUNC1:78

    f is convergent_in-infty implies (( lim_in-infty f) = g iff for g1 st 0 < g1 holds ex r st for r1 st r1 < r & r1 in ( dom f) holds |.((f . r1) - g).| < g1)

    proof

      assume

       A1: f is convergent_in-infty;

      thus ( lim_in-infty f) = g implies for g1 st 0 < g1 holds ex r st for r1 st r1 < r & r1 in ( dom f) holds |.((f . r1) - g).| < g1

      proof

        deffunc U( Nat) = ( - $1);

        assume

         A2: ( lim_in-infty f) = g;

        consider s1 be Real_Sequence such that

         A3: for n holds (s1 . n) = U(n) from SEQ_1:sch 1;

        given g1 such that

         A4: 0 < g1 and

         A5: for r holds ex r1 st r1 < r & r1 in ( dom f) & |.((f . r1) - g).| >= g1;

        defpred X[ Nat, Real] means $2 < ( - $1) & $2 in ( dom f) & |.((f . $2) - g).| >= g1;

        

         A6: for n be Element of NAT holds ex r be Element of REAL st X[n, r]

        proof

          let n be Element of NAT ;

          consider r such that

           A7: X[n, r] by A5;

          reconsider r as Real;

           X[n, r] by A7;

          hence thesis;

        end;

        consider s be Real_Sequence such that

         A8: for n be Element of NAT holds X[n, (s . n)] from FUNCT_2:sch 3( A6);

        now

          let x be object;

          assume x in ( rng s);

          then ex n be Element of NAT st (s . n) = x by FUNCT_2: 113;

          hence x in ( dom f) by A8;

        end;

        then

         A9: ( rng s) c= ( dom f);

        now

          let n;

          n in NAT by ORDINAL1:def 12;

          then (s . n) < ( - n) by A8;

          hence (s . n) <= (s1 . n) by A3;

        end;

        then s is divergent_to-infty by A3, Th21, Th43;

        then (f /* s) is convergent & ( lim (f /* s)) = g by A1, A2, A9, Def13;

        then

        consider n such that

         A10: for m st n <= m holds |.(((f /* s) . m) - g).| < g1 by A4, SEQ_2:def 7;

        

         A11: n in NAT by ORDINAL1:def 12;

         |.(((f /* s) . n) - g).| < g1 by A10;

        then |.((f . (s . n)) - g).| < g1 by A9, FUNCT_2: 108, A11;

        hence contradiction by A8, A11;

      end;

      assume

       A12: for g1 st 0 < g1 holds ex r st for r1 st r1 < r & r1 in ( dom f) holds |.((f . r1) - g).| < g1;

      reconsider g as Real;

      now

        let s be Real_Sequence such that

         A13: s is divergent_to-infty and

         A14: ( rng s) c= ( dom f);

         A15:

        now

          let g1 be Real;

          assume

           A16: 0 < g1;

          consider r such that

           A17: for r1 st r1 < r & r1 in ( dom f) holds |.((f . r1) - g).| < g1 by A12, A16;

          consider n such that

           A18: for m st n <= m holds (s . m) < r by A13;

          take n;

          let m;

          

           A19: (s . m) in ( rng s) by VALUED_0: 28;

          

           A20: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then |.((f . (s . m)) - g).| < g1 by A14, A17, A18, A19;

          hence |.(((f /* s) . m) - g).| < g1 by A14, FUNCT_2: 108, A20;

        end;

        hence (f /* s) is convergent;

        hence ( lim (f /* s)) = g by A15, SEQ_2:def 7;

      end;

      hence thesis by A1, Def13;

    end;

    theorem :: LIMFUNC1:79

    f is convergent_in+infty implies (( lim_in+infty f) = g iff for g1 st 0 < g1 holds ex r st for r1 st r < r1 & r1 in ( dom f) holds |.((f . r1) - g).| < g1)

    proof

      assume

       A1: f is convergent_in+infty;

      thus ( lim_in+infty f) = g implies for g1 st 0 < g1 holds ex r st for r1 st r < r1 & r1 in ( dom f) holds |.((f . r1) - g).| < g1

      proof

        assume

         A2: ( lim_in+infty f) = g;

        given g1 such that

         A3: 0 < g1 and

         A4: for r holds ex r1 st r < r1 & r1 in ( dom f) & |.((f . r1) - g).| >= g1;

        defpred X[ Nat, Real] means $1 < $2 & $2 in ( dom f) & |.((f . $2) - g).| >= g1;

        

         A5: for n be Element of NAT holds ex r be Element of REAL st X[n, r]

        proof

          let n be Element of NAT ;

          consider r such that

           A6: X[n, r] by A4;

          reconsider r as Real;

           X[n, r] by A6;

          hence thesis;

        end;

        consider s be Real_Sequence such that

         A7: for n be Element of NAT holds X[n, (s . n)] from FUNCT_2:sch 3( A5);

        now

          let x be object;

          assume x in ( rng s);

          then ex n be Element of NAT st (s . n) = x by FUNCT_2: 113;

          hence x in ( dom f) by A7;

        end;

        then

         A8: ( rng s) c= ( dom f);

        now

          let n;

          

           A9: n in NAT by ORDINAL1:def 12;

          then n < (s . n) by A7;

          hence (s1 . n) <= (s . n) by FUNCT_1: 18, A9;

        end;

        then s is divergent_to+infty by Lm5, Th20, Th42;

        then (f /* s) is convergent & ( lim (f /* s)) = g by A1, A2, A8, Def12;

        then

        consider n such that

         A10: for m st n <= m holds |.(((f /* s) . m) - g).| < g1 by A3, SEQ_2:def 7;

        

         A11: n in NAT by ORDINAL1:def 12;

         |.(((f /* s) . n) - g).| < g1 by A10;

        then |.((f . (s . n)) - g).| < g1 by A8, FUNCT_2: 108, A11;

        hence contradiction by A7, A11;

      end;

      assume

       A12: for g1 st 0 < g1 holds ex r st for r1 st r < r1 & r1 in ( dom f) holds |.((f . r1) - g).| < g1;

      reconsider g as Real;

      now

        let s be Real_Sequence such that

         A13: s is divergent_to+infty and

         A14: ( rng s) c= ( dom f);

         A15:

        now

          let g1 be Real;

          assume

           A16: 0 < g1;

          consider r such that

           A17: for r1 st r < r1 & r1 in ( dom f) holds |.((f . r1) - g).| < g1 by A12, A16;

          consider n such that

           A18: for m st n <= m holds r < (s . m) by A13;

          take n;

          let m;

          

           A19: (s . m) in ( rng s) by VALUED_0: 28;

          

           A20: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then |.((f . (s . m)) - g).| < g1 by A14, A17, A18, A19;

          hence |.(((f /* s) . m) - g).| < g1 by A14, FUNCT_2: 108, A20;

        end;

        hence (f /* s) is convergent;

        hence ( lim (f /* s)) = g by A15, SEQ_2:def 7;

      end;

      hence thesis by A1, Def12;

    end;

    theorem :: LIMFUNC1:80

    

     Th80: f is convergent_in+infty implies (r (#) f) is convergent_in+infty & ( lim_in+infty (r (#) f)) = (r * ( lim_in+infty f))

    proof

      assume

       A1: f is convergent_in+infty;

       A2:

      now

        let seq;

        assume that

         A3: seq is divergent_to+infty and

         A4: ( rng seq) c= ( dom (r (#) f));

        

         A5: ( rng seq) c= ( dom f) by A4, VALUED_1:def 5;

        then

         A6: ( lim (f /* seq)) = ( lim_in+infty f) by A1, A3, Def12;

        

         A7: (f /* seq) is convergent by A1, A3, A5;

        then (r (#) (f /* seq)) is convergent;

        hence ((r (#) f) /* seq) is convergent by A5, RFUNCT_2: 9;

        

        thus ( lim ((r (#) f) /* seq)) = ( lim (r (#) (f /* seq))) by A5, RFUNCT_2: 9

        .= (r * ( lim_in+infty f)) by A7, A6, SEQ_2: 8;

      end;

      for r1 holds ex g st r1 < g & g in ( dom (r (#) f))

      proof

        let r1;

        consider g such that

         A8: r1 < g & g in ( dom f) by A1;

        take g;

        thus thesis by A8, VALUED_1:def 5;

      end;

      hence (r (#) f) is convergent_in+infty by A2;

      hence thesis by A2, Def12;

    end;

    theorem :: LIMFUNC1:81

    

     Th81: f is convergent_in+infty implies ( - f) is convergent_in+infty & ( lim_in+infty ( - f)) = ( - ( lim_in+infty f))

    proof

      assume

       A1: f is convergent_in+infty;

      thus ( - f) is convergent_in+infty by A1, Th80;

      

      thus ( lim_in+infty ( - f)) = (( - jj) * ( lim_in+infty f)) by A1, Th80

      .= ( - ( lim_in+infty f));

    end;

    theorem :: LIMFUNC1:82

    

     Th82: f1 is convergent_in+infty & f2 is convergent_in+infty & (for r holds ex g st r < g & g in ( dom (f1 + f2))) implies (f1 + f2) is convergent_in+infty & ( lim_in+infty (f1 + f2)) = (( lim_in+infty f1) + ( lim_in+infty f2))

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is convergent_in+infty and

       A3: for r holds ex g st r < g & g in ( dom (f1 + f2));

       A4:

      now

        let seq;

        assume that

         A5: seq is divergent_to+infty and

         A6: ( rng seq) c= ( dom (f1 + f2));

        

         A7: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by A6, Lm2;

        

         A8: ( rng seq) c= ( dom f2) by A6, Lm2;

        then

         A9: ( lim (f2 /* seq)) = ( lim_in+infty f2) by A2, A5, Def12;

        

         A10: (f2 /* seq) is convergent by A2, A5, A8;

        

         A11: ( rng seq) c= ( dom f1) by A6, Lm2;

        then

         A12: ( lim (f1 /* seq)) = ( lim_in+infty f1) by A1, A5, Def12;

        

         A13: (f1 /* seq) is convergent by A1, A5, A11;

        then ((f1 /* seq) + (f2 /* seq)) is convergent by A10;

        hence ((f1 + f2) /* seq) is convergent by A6, A7, RFUNCT_2: 8;

        

        thus ( lim ((f1 + f2) /* seq)) = ( lim ((f1 /* seq) + (f2 /* seq))) by A6, A7, RFUNCT_2: 8

        .= (( lim_in+infty f1) + ( lim_in+infty f2)) by A13, A12, A10, A9, SEQ_2: 6;

      end;

      hence (f1 + f2) is convergent_in+infty by A3;

      hence thesis by A4, Def12;

    end;

    theorem :: LIMFUNC1:83

    f1 is convergent_in+infty & f2 is convergent_in+infty & (for r holds ex g st r < g & g in ( dom (f1 - f2))) implies (f1 - f2) is convergent_in+infty & ( lim_in+infty (f1 - f2)) = (( lim_in+infty f1) - ( lim_in+infty f2))

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is convergent_in+infty and

       A3: for r holds ex g st r < g & g in ( dom (f1 - f2));

      

       A4: ( - f2) is convergent_in+infty by A2, Th81;

      hence (f1 - f2) is convergent_in+infty by A1, A3, Th82;

      ( lim_in+infty ( - f2)) = ( - ( lim_in+infty f2)) by A2, Th81;

      

      hence ( lim_in+infty (f1 - f2)) = (( lim_in+infty f1) + ( - ( lim_in+infty f2))) by A1, A3, A4, Th82

      .= (( lim_in+infty f1) - ( lim_in+infty f2));

    end;

    theorem :: LIMFUNC1:84

    f is convergent_in+infty & (f " { 0 }) = {} & ( lim_in+infty f) <> 0 implies (f ^ ) is convergent_in+infty & ( lim_in+infty (f ^ )) = (( lim_in+infty f) " )

    proof

      assume that

       A1: f is convergent_in+infty and

       A2: (f " { 0 }) = {} and

       A3: ( lim_in+infty f) <> 0 ;

      

       A4: ( dom f) = (( dom f) \ (f " { 0 })) by A2

      .= ( dom (f ^ )) by RFUNCT_1:def 2;

       A5:

      now

        let seq;

        assume that

         A6: seq is divergent_to+infty and

         A7: ( rng seq) c= ( dom (f ^ ));

        

         A8: (f /* seq) is convergent & ( lim (f /* seq)) = ( lim_in+infty f) by A1, A4, A6, A7, Def12;

        then ((f /* seq) " ) is convergent by A3, A7, RFUNCT_2: 11, SEQ_2: 21;

        hence ((f ^ ) /* seq) is convergent by A7, RFUNCT_2: 12;

        

        thus ( lim ((f ^ ) /* seq)) = ( lim ((f /* seq) " )) by A7, RFUNCT_2: 12

        .= (( lim_in+infty f) " ) by A3, A7, A8, RFUNCT_2: 11, SEQ_2: 22;

      end;

      for r holds ex g st r < g & g in ( dom (f ^ )) by A1, A4;

      hence (f ^ ) is convergent_in+infty by A5;

      hence thesis by A5, Def12;

    end;

    theorem :: LIMFUNC1:85

    f is convergent_in+infty implies ( abs f) is convergent_in+infty & ( lim_in+infty ( abs f)) = |.( lim_in+infty f).|

    proof

      assume

       A1: f is convergent_in+infty;

       A2:

      now

        let seq;

        assume that

         A3: seq is divergent_to+infty and

         A4: ( rng seq) c= ( dom ( abs f));

        

         A5: ( rng seq) c= ( dom f) by A4, VALUED_1:def 11;

        then

         A6: ( lim (f /* seq)) = ( lim_in+infty f) by A1, A3, Def12;

        

         A7: (f /* seq) is convergent by A1, A3, A5;

        then ( abs (f /* seq)) is convergent;

        hence (( abs f) /* seq) is convergent by A5, RFUNCT_2: 10;

        

        thus ( lim (( abs f) /* seq)) = ( lim ( abs (f /* seq))) by A5, RFUNCT_2: 10

        .= |.( lim_in+infty f).| by A7, A6, SEQ_4: 14;

      end;

      now

        let r;

        consider g such that

         A8: r < g & g in ( dom f) by A1;

        take g;

        thus r < g & g in ( dom ( abs f)) by A8, VALUED_1:def 11;

      end;

      hence ( abs f) is convergent_in+infty by A2;

      hence thesis by A2, Def12;

    end;

    theorem :: LIMFUNC1:86

    

     Th86: f is convergent_in+infty & ( lim_in+infty f) <> 0 & (for r holds ex g st r < g & g in ( dom f) & (f . g) <> 0 ) implies (f ^ ) is convergent_in+infty & ( lim_in+infty (f ^ )) = (( lim_in+infty f) " )

    proof

      assume that

       A1: f is convergent_in+infty and

       A2: ( lim_in+infty f) <> 0 and

       A3: for r holds ex g st r < g & g in ( dom f) & (f . g) <> 0 ;

       A4:

      now

        let seq such that

         A5: seq is divergent_to+infty and

         A6: ( rng seq) c= ( dom (f ^ ));

        ( dom (f ^ )) = (( dom f) \ (f " { 0 })) & (( dom f) \ (f " { 0 })) c= ( dom f) by RFUNCT_1:def 2, XBOOLE_1: 36;

        then ( rng seq) c= ( dom f) by A6;

        then

         A7: (f /* seq) is convergent & ( lim (f /* seq)) = ( lim_in+infty f) by A1, A5, Def12;

        then ((f /* seq) " ) is convergent by A2, A6, RFUNCT_2: 11, SEQ_2: 21;

        hence ((f ^ ) /* seq) is convergent by A6, RFUNCT_2: 12;

        

        thus ( lim ((f ^ ) /* seq)) = ( lim ((f /* seq) " )) by A6, RFUNCT_2: 12

        .= (( lim_in+infty f) " ) by A2, A6, A7, RFUNCT_2: 11, SEQ_2: 22;

      end;

      now

        let r;

        consider g such that

         A8: r < g and

         A9: g in ( dom f) and

         A10: (f . g) <> 0 by A3;

        take g;

         not (f . g) in { 0 } by A10, TARSKI:def 1;

        then not g in (f " { 0 }) by FUNCT_1:def 7;

        then g in (( dom f) \ (f " { 0 })) by A9, XBOOLE_0:def 5;

        hence r < g & g in ( dom (f ^ )) by A8, RFUNCT_1:def 2;

      end;

      hence (f ^ ) is convergent_in+infty by A4;

      hence thesis by A4, Def12;

    end;

    theorem :: LIMFUNC1:87

    

     Th87: f1 is convergent_in+infty & f2 is convergent_in+infty & (for r holds ex g st r < g & g in ( dom (f1 (#) f2))) implies (f1 (#) f2) is convergent_in+infty & ( lim_in+infty (f1 (#) f2)) = (( lim_in+infty f1) * ( lim_in+infty f2))

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is convergent_in+infty and

       A3: for r holds ex g st r < g & g in ( dom (f1 (#) f2));

       A4:

      now

        let seq;

        assume that

         A5: seq is divergent_to+infty and

         A6: ( rng seq) c= ( dom (f1 (#) f2));

        

         A7: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by A6, Lm3;

        

         A8: ( rng seq) c= ( dom f2) by A6, Lm3;

        then

         A9: ( lim (f2 /* seq)) = ( lim_in+infty f2) by A2, A5, Def12;

        

         A10: (f2 /* seq) is convergent by A2, A5, A8;

        

         A11: ( rng seq) c= ( dom f1) by A6, Lm3;

        then

         A12: ( lim (f1 /* seq)) = ( lim_in+infty f1) by A1, A5, Def12;

        

         A13: (f1 /* seq) is convergent by A1, A5, A11;

        then ((f1 /* seq) (#) (f2 /* seq)) is convergent by A10;

        hence ((f1 (#) f2) /* seq) is convergent by A6, A7, RFUNCT_2: 8;

        

        thus ( lim ((f1 (#) f2) /* seq)) = ( lim ((f1 /* seq) (#) (f2 /* seq))) by A6, A7, RFUNCT_2: 8

        .= (( lim_in+infty f1) * ( lim_in+infty f2)) by A13, A12, A10, A9, SEQ_2: 15;

      end;

      hence (f1 (#) f2) is convergent_in+infty by A3;

      hence thesis by A4, Def12;

    end;

    theorem :: LIMFUNC1:88

    f1 is convergent_in+infty & f2 is convergent_in+infty & ( lim_in+infty f2) <> 0 & (for r holds ex g st r < g & g in ( dom (f1 / f2))) implies (f1 / f2) is convergent_in+infty & ( lim_in+infty (f1 / f2)) = (( lim_in+infty f1) / ( lim_in+infty f2))

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is convergent_in+infty & ( lim_in+infty f2) <> 0 and

       A3: for r holds ex g st r < g & g in ( dom (f1 / f2));

      ( dom (f1 / f2)) = (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by RFUNCT_1:def 1;

      then

       A4: ( dom (f1 / f2)) = (( dom f1) /\ ( dom (f2 ^ ))) by RFUNCT_1:def 2;

      

       A5: (( dom f1) /\ ( dom (f2 ^ ))) c= ( dom (f2 ^ )) by XBOOLE_1: 17;

       A6:

      now

        let r;

        consider g such that

         A7: r < g and

         A8: g in ( dom (f1 / f2)) by A3;

        take g;

        g in ( dom (f2 ^ )) by A4, A5, A8;

        then

         A9: g in (( dom f2) \ (f2 " { 0 })) by RFUNCT_1:def 2;

        then g in ( dom f2) & not g in (f2 " { 0 }) by XBOOLE_0:def 5;

        then not (f2 . g) in { 0 } by FUNCT_1:def 7;

        hence r < g & g in ( dom f2) & (f2 . g) <> 0 by A7, A9, TARSKI:def 1, XBOOLE_0:def 5;

      end;

      then

       A10: (f2 ^ ) is convergent_in+infty by A2, Th86;

      

       A11: ( lim_in+infty (f2 ^ )) = (( lim_in+infty f2) " ) by A2, A6, Th86;

       A12:

      now

        let r;

        consider g such that

         A13: r < g & g in ( dom (f1 / f2)) by A3;

        take g;

        thus r < g & g in ( dom (f1 (#) (f2 ^ ))) by A4, A13, VALUED_1:def 4;

      end;

      then (f1 (#) (f2 ^ )) is convergent_in+infty by A1, A10, Th87;

      hence (f1 / f2) is convergent_in+infty by RFUNCT_1: 31;

      

      thus ( lim_in+infty (f1 / f2)) = ( lim_in+infty (f1 (#) (f2 ^ ))) by RFUNCT_1: 31

      .= (( lim_in+infty f1) * (( lim_in+infty f2) " )) by A1, A12, A10, A11, Th87

      .= (( lim_in+infty f1) / ( lim_in+infty f2)) by XCMPLX_0:def 9;

    end;

    theorem :: LIMFUNC1:89

    

     Th89: f is convergent_in-infty implies (r (#) f) is convergent_in-infty & ( lim_in-infty (r (#) f)) = (r * ( lim_in-infty f))

    proof

      assume

       A1: f is convergent_in-infty;

       A2:

      now

        let seq;

        assume that

         A3: seq is divergent_to-infty and

         A4: ( rng seq) c= ( dom (r (#) f));

        

         A5: ( rng seq) c= ( dom f) by A4, VALUED_1:def 5;

        then

         A6: ( lim (f /* seq)) = ( lim_in-infty f) by A1, A3, Def13;

        

         A7: (f /* seq) is convergent by A1, A3, A5;

        then (r (#) (f /* seq)) is convergent;

        hence ((r (#) f) /* seq) is convergent by A5, RFUNCT_2: 9;

        

        thus ( lim ((r (#) f) /* seq)) = ( lim (r (#) (f /* seq))) by A5, RFUNCT_2: 9

        .= (r * ( lim_in-infty f)) by A7, A6, SEQ_2: 8;

      end;

      for r1 holds ex g st g < r1 & g in ( dom (r (#) f))

      proof

        let r1;

        consider g such that

         A8: g < r1 & g in ( dom f) by A1;

        take g;

        thus thesis by A8, VALUED_1:def 5;

      end;

      hence (r (#) f) is convergent_in-infty by A2;

      hence thesis by A2, Def13;

    end;

    theorem :: LIMFUNC1:90

    

     Th90: f is convergent_in-infty implies ( - f) is convergent_in-infty & ( lim_in-infty ( - f)) = ( - ( lim_in-infty f))

    proof

      assume

       A1: f is convergent_in-infty;

      thus ( - f) is convergent_in-infty by A1, Th89;

      

      thus ( lim_in-infty ( - f)) = (( - jj) * ( lim_in-infty f)) by A1, Th89

      .= ( - ( lim_in-infty f));

    end;

    theorem :: LIMFUNC1:91

    

     Th91: f1 is convergent_in-infty & f2 is convergent_in-infty & (for r holds ex g st g < r & g in ( dom (f1 + f2))) implies (f1 + f2) is convergent_in-infty & ( lim_in-infty (f1 + f2)) = (( lim_in-infty f1) + ( lim_in-infty f2))

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is convergent_in-infty and

       A3: for r holds ex g st g < r & g in ( dom (f1 + f2));

       A4:

      now

        let seq;

        assume that

         A5: seq is divergent_to-infty and

         A6: ( rng seq) c= ( dom (f1 + f2));

        

         A7: ( rng seq) c= (( dom f1) /\ ( dom f2)) by A6, VALUED_1:def 1;

        (( dom f1) /\ ( dom f2)) c= ( dom f2) by XBOOLE_1: 17;

        then

         A8: ( rng seq) c= ( dom f2) by A7;

        then

         A9: ( lim (f2 /* seq)) = ( lim_in-infty f2) by A2, A5, Def13;

        

         A10: (f2 /* seq) is convergent by A2, A5, A8;

        (( dom f1) /\ ( dom f2)) c= ( dom f1) by XBOOLE_1: 17;

        then

         A11: ( rng seq) c= ( dom f1) by A7;

        then

         A12: ( lim (f1 /* seq)) = ( lim_in-infty f1) by A1, A5, Def13;

        

         A13: (f1 /* seq) is convergent by A1, A5, A11;

        then ((f1 /* seq) + (f2 /* seq)) is convergent by A10;

        hence ((f1 + f2) /* seq) is convergent by A7, RFUNCT_2: 8;

        

        thus ( lim ((f1 + f2) /* seq)) = ( lim ((f1 /* seq) + (f2 /* seq))) by A7, RFUNCT_2: 8

        .= (( lim_in-infty f1) + ( lim_in-infty f2)) by A13, A12, A10, A9, SEQ_2: 6;

      end;

      hence (f1 + f2) is convergent_in-infty by A3;

      hence thesis by A4, Def13;

    end;

    theorem :: LIMFUNC1:92

    f1 is convergent_in-infty & f2 is convergent_in-infty & (for r holds ex g st g < r & g in ( dom (f1 - f2))) implies (f1 - f2) is convergent_in-infty & ( lim_in-infty (f1 - f2)) = (( lim_in-infty f1) - ( lim_in-infty f2))

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is convergent_in-infty and

       A3: for r holds ex g st g < r & g in ( dom (f1 - f2));

      

       A4: ( - f2) is convergent_in-infty by A2, Th90;

      hence (f1 - f2) is convergent_in-infty by A1, A3, Th91;

      ( lim_in-infty ( - f2)) = ( - ( lim_in-infty f2)) by A2, Th90;

      

      hence ( lim_in-infty (f1 - f2)) = (( lim_in-infty f1) + ( - ( lim_in-infty f2))) by A1, A3, A4, Th91

      .= (( lim_in-infty f1) - ( lim_in-infty f2));

    end;

    theorem :: LIMFUNC1:93

    f is convergent_in-infty & (f " { 0 }) = {} & ( lim_in-infty f) <> 0 implies (f ^ ) is convergent_in-infty & ( lim_in-infty (f ^ )) = (( lim_in-infty f) " )

    proof

      assume that

       A1: f is convergent_in-infty and

       A2: (f " { 0 }) = {} and

       A3: ( lim_in-infty f) <> 0 ;

      

       A4: ( dom f) = (( dom f) \ (f " { 0 })) by A2

      .= ( dom (f ^ )) by RFUNCT_1:def 2;

       A5:

      now

        let seq;

        assume that

         A6: seq is divergent_to-infty and

         A7: ( rng seq) c= ( dom (f ^ ));

        

         A8: (f /* seq) is convergent & ( lim (f /* seq)) = ( lim_in-infty f) by A1, A4, A6, A7, Def13;

        then ((f /* seq) " ) is convergent by A3, A7, RFUNCT_2: 11, SEQ_2: 21;

        hence ((f ^ ) /* seq) is convergent by A7, RFUNCT_2: 12;

        

        thus ( lim ((f ^ ) /* seq)) = ( lim ((f /* seq) " )) by A7, RFUNCT_2: 12

        .= (( lim_in-infty f) " ) by A3, A7, A8, RFUNCT_2: 11, SEQ_2: 22;

      end;

      for r holds ex g st g < r & g in ( dom (f ^ )) by A1, A4;

      hence (f ^ ) is convergent_in-infty by A5;

      hence thesis by A5, Def13;

    end;

    theorem :: LIMFUNC1:94

    f is convergent_in-infty implies ( abs f) is convergent_in-infty & ( lim_in-infty ( abs f)) = |.( lim_in-infty f).|

    proof

      assume

       A1: f is convergent_in-infty;

       A2:

      now

        let seq;

        assume that

         A3: seq is divergent_to-infty and

         A4: ( rng seq) c= ( dom ( abs f));

        

         A5: ( rng seq) c= ( dom f) by A4, VALUED_1:def 11;

        then

         A6: ( lim (f /* seq)) = ( lim_in-infty f) by A1, A3, Def13;

        

         A7: (f /* seq) is convergent by A1, A3, A5;

        then ( abs (f /* seq)) is convergent;

        hence (( abs f) /* seq) is convergent by A5, RFUNCT_2: 10;

        

        thus ( lim (( abs f) /* seq)) = ( lim ( abs (f /* seq))) by A5, RFUNCT_2: 10

        .= |.( lim_in-infty f).| by A7, A6, SEQ_4: 14;

      end;

      now

        let r;

        consider g such that

         A8: g < r & g in ( dom f) by A1;

        take g;

        thus g < r & g in ( dom ( abs f)) by A8, VALUED_1:def 11;

      end;

      hence ( abs f) is convergent_in-infty by A2;

      hence thesis by A2, Def13;

    end;

    theorem :: LIMFUNC1:95

    

     Th95: f is convergent_in-infty & ( lim_in-infty f) <> 0 & (for r holds ex g st g < r & g in ( dom f) & (f . g) <> 0 ) implies (f ^ ) is convergent_in-infty & ( lim_in-infty (f ^ )) = (( lim_in-infty f) " )

    proof

      assume that

       A1: f is convergent_in-infty and

       A2: ( lim_in-infty f) <> 0 and

       A3: for r holds ex g st g < r & g in ( dom f) & (f . g) <> 0 ;

       A4:

      now

        let seq such that

         A5: seq is divergent_to-infty and

         A6: ( rng seq) c= ( dom (f ^ ));

        ( dom (f ^ )) = (( dom f) \ (f " { 0 })) & (( dom f) \ (f " { 0 })) c= ( dom f) by RFUNCT_1:def 2, XBOOLE_1: 36;

        then ( rng seq) c= ( dom f) by A6;

        then

         A7: (f /* seq) is convergent & ( lim (f /* seq)) = ( lim_in-infty f) by A1, A5, Def13;

        then ((f /* seq) " ) is convergent by A2, A6, RFUNCT_2: 11, SEQ_2: 21;

        hence ((f ^ ) /* seq) is convergent by A6, RFUNCT_2: 12;

        

        thus ( lim ((f ^ ) /* seq)) = ( lim ((f /* seq) " )) by A6, RFUNCT_2: 12

        .= (( lim_in-infty f) " ) by A2, A6, A7, RFUNCT_2: 11, SEQ_2: 22;

      end;

      now

        let r;

        consider g such that

         A8: g < r and

         A9: g in ( dom f) and

         A10: (f . g) <> 0 by A3;

        take g;

         not (f . g) in { 0 } by A10, TARSKI:def 1;

        then not g in (f " { 0 }) by FUNCT_1:def 7;

        then g in (( dom f) \ (f " { 0 })) by A9, XBOOLE_0:def 5;

        hence g < r & g in ( dom (f ^ )) by A8, RFUNCT_1:def 2;

      end;

      hence (f ^ ) is convergent_in-infty by A4;

      hence thesis by A4, Def13;

    end;

    theorem :: LIMFUNC1:96

    

     Th96: f1 is convergent_in-infty & f2 is convergent_in-infty & (for r holds ex g st g < r & g in ( dom (f1 (#) f2))) implies (f1 (#) f2) is convergent_in-infty & ( lim_in-infty (f1 (#) f2)) = (( lim_in-infty f1) * ( lim_in-infty f2))

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is convergent_in-infty and

       A3: for r holds ex g st g < r & g in ( dom (f1 (#) f2));

       A4:

      now

        let seq;

        assume that

         A5: seq is divergent_to-infty and

         A6: ( rng seq) c= ( dom (f1 (#) f2));

        

         A7: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

        (( dom f1) /\ ( dom f2)) c= ( dom f2) by XBOOLE_1: 17;

        then

         A8: ( rng seq) c= ( dom f2) by A6, A7;

        then

         A9: ( lim (f2 /* seq)) = ( lim_in-infty f2) by A2, A5, Def13;

        

         A10: (f2 /* seq) is convergent by A2, A5, A8;

        (( dom f1) /\ ( dom f2)) c= ( dom f1) by XBOOLE_1: 17;

        then

         A11: ( rng seq) c= ( dom f1) by A6, A7;

        then

         A12: ( lim (f1 /* seq)) = ( lim_in-infty f1) by A1, A5, Def13;

        

         A13: (f1 /* seq) is convergent by A1, A5, A11;

        then ((f1 /* seq) (#) (f2 /* seq)) is convergent by A10;

        hence ((f1 (#) f2) /* seq) is convergent by A6, A7, RFUNCT_2: 8;

        

        thus ( lim ((f1 (#) f2) /* seq)) = ( lim ((f1 /* seq) (#) (f2 /* seq))) by A6, A7, RFUNCT_2: 8

        .= (( lim_in-infty f1) * ( lim_in-infty f2)) by A13, A12, A10, A9, SEQ_2: 15;

      end;

      hence (f1 (#) f2) is convergent_in-infty by A3;

      hence thesis by A4, Def13;

    end;

    theorem :: LIMFUNC1:97

    f1 is convergent_in-infty & f2 is convergent_in-infty & ( lim_in-infty f2) <> 0 & (for r holds ex g st g < r & g in ( dom (f1 / f2))) implies (f1 / f2) is convergent_in-infty & ( lim_in-infty (f1 / f2)) = (( lim_in-infty f1) / ( lim_in-infty f2))

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is convergent_in-infty & ( lim_in-infty f2) <> 0 and

       A3: for r holds ex g st g < r & g in ( dom (f1 / f2));

      ( dom (f1 / f2)) = (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by RFUNCT_1:def 1;

      then

       A4: ( dom (f1 / f2)) = (( dom f1) /\ ( dom (f2 ^ ))) by RFUNCT_1:def 2;

      

       A5: (( dom f1) /\ ( dom (f2 ^ ))) c= ( dom (f2 ^ )) by XBOOLE_1: 17;

       A6:

      now

        let r;

        consider g such that

         A7: g < r and

         A8: g in ( dom (f1 / f2)) by A3;

        take g;

        g in ( dom (f2 ^ )) by A4, A5, A8;

        then

         A9: g in (( dom f2) \ (f2 " { 0 })) by RFUNCT_1:def 2;

        then g in ( dom f2) & not g in (f2 " { 0 }) by XBOOLE_0:def 5;

        then not (f2 . g) in { 0 } by FUNCT_1:def 7;

        hence g < r & g in ( dom f2) & (f2 . g) <> 0 by A7, A9, TARSKI:def 1, XBOOLE_0:def 5;

      end;

      then

       A10: (f2 ^ ) is convergent_in-infty by A2, Th95;

      

       A11: ( lim_in-infty (f2 ^ )) = (( lim_in-infty f2) " ) by A2, A6, Th95;

       A12:

      now

        let r;

        consider g such that

         A13: g < r & g in ( dom (f1 / f2)) by A3;

        take g;

        thus g < r & g in ( dom (f1 (#) (f2 ^ ))) by A4, A13, VALUED_1:def 4;

      end;

      then (f1 (#) (f2 ^ )) is convergent_in-infty by A1, A10, Th96;

      hence (f1 / f2) is convergent_in-infty by RFUNCT_1: 31;

      

      thus ( lim_in-infty (f1 / f2)) = ( lim_in-infty (f1 (#) (f2 ^ ))) by RFUNCT_1: 31

      .= (( lim_in-infty f1) * (( lim_in-infty f2) " )) by A1, A12, A10, A11, Th96

      .= (( lim_in-infty f1) / ( lim_in-infty f2)) by XCMPLX_0:def 9;

    end;

    theorem :: LIMFUNC1:98

    f1 is convergent_in+infty & ( lim_in+infty f1) = 0 & (for r holds ex g st r < g & g in ( dom (f1 (#) f2))) & (ex r st (f2 | ( right_open_halfline r)) is bounded) implies (f1 (#) f2) is convergent_in+infty & ( lim_in+infty (f1 (#) f2)) = 0

    proof

      assume that

       A1: f1 is convergent_in+infty & ( lim_in+infty f1) = 0 and

       A2: for r holds ex g st r < g & g in ( dom (f1 (#) f2));

      given r such that

       A3: (f2 | ( right_open_halfline r)) is bounded;

      consider g be Real such that

       A4: for r1 be object st r1 in (( right_open_halfline r) /\ ( dom f2)) holds |.(f2 . r1).| <= g by A3, RFUNCT_1: 73;

       A5:

      now

        let s be Real_Sequence;

        assume that

         A6: s is divergent_to+infty and

         A7: ( rng s) c= ( dom (f1 (#) f2));

        consider k such that

         A8: for n st k <= n holds r < (s . n) by A6;

        

         A9: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

        

         A10: ( rng s) c= ( dom f2) by A7, Lm3;

        then

         A11: ( rng (s ^\ k)) c= ( dom f2) by A9;

        now

          set t = ( |.g.| + 1);

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

          hence 0 < t;

          let n;

          

           A12: n in NAT by ORDINAL1:def 12;

          r < (s . (n + k)) by A8, NAT_1: 12;

          then r < ((s ^\ k) . n) by NAT_1:def 3;

          then ((s ^\ k) . n) in { g1 : r < g1 };

          then ((s ^\ k) . n) in ( rng (s ^\ k)) & ((s ^\ k) . n) in ( right_open_halfline r) by VALUED_0: 28, XXREAL_1: 230;

          then ((s ^\ k) . n) in (( right_open_halfline r) /\ ( dom f2)) by A11, XBOOLE_0:def 4;

          then |.(f2 . ((s ^\ k) . n)).| <= g by A4;

          then

           A13: |.((f2 /* (s ^\ k)) . n).| <= g by A10, A9, FUNCT_2: 108, XBOOLE_1: 1, A12;

          g <= |.g.| by ABSVALUE: 4;

          then g < t by Lm1;

          hence |.((f2 /* (s ^\ k)) . n).| < t by A13, XXREAL_0: 2;

        end;

        then

         A14: (f2 /* (s ^\ k)) is bounded by SEQ_2: 3;

        ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by A7, Lm3;

        then ( rng (s ^\ k)) c= (( dom f1) /\ ( dom f2)) by A7, A9;

        

        then

         A15: ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) = ((f1 (#) f2) /* (s ^\ k)) by RFUNCT_2: 8

        .= (((f1 (#) f2) /* s) ^\ k) by A7, VALUED_0: 27;

        ( rng s) c= ( dom f1) by A7, Lm3;

        then

         A16: ( rng (s ^\ k)) c= ( dom f1) by A9;

        (s ^\ k) is divergent_to+infty by A6, Th26;

        then

         A17: (f1 /* (s ^\ k)) is convergent & ( lim (f1 /* (s ^\ k))) = 0 by A1, A16, Def12;

        then

         A18: ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) is convergent by A14, SEQ_2: 25;

        hence ((f1 (#) f2) /* s) is convergent by A15, SEQ_4: 21;

        ( lim ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)))) = 0 by A17, A14, SEQ_2: 26;

        hence ( lim ((f1 (#) f2) /* s)) = 0 by A18, A15, SEQ_4: 22;

      end;

      hence (f1 (#) f2) is convergent_in+infty by A2;

      hence thesis by A5, Def12;

    end;

    theorem :: LIMFUNC1:99

    f1 is convergent_in-infty & ( lim_in-infty f1) = 0 & (for r holds ex g st g < r & g in ( dom (f1 (#) f2))) & (ex r st (f2 | ( left_open_halfline r)) is bounded) implies (f1 (#) f2) is convergent_in-infty & ( lim_in-infty (f1 (#) f2)) = 0

    proof

      assume that

       A1: f1 is convergent_in-infty & ( lim_in-infty f1) = 0 and

       A2: for r holds ex g st g < r & g in ( dom (f1 (#) f2));

      given r such that

       A3: (f2 | ( left_open_halfline r)) is bounded;

      consider g be Real such that

       A4: for r1 be object st r1 in (( left_open_halfline r) /\ ( dom f2)) holds |.(f2 . r1).| <= g by A3, RFUNCT_1: 73;

       A5:

      now

        let s be Real_Sequence;

        assume that

         A6: s is divergent_to-infty and

         A7: ( rng s) c= ( dom (f1 (#) f2));

        consider k such that

         A8: for n st k <= n holds (s . n) < r by A6;

        

         A9: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

        

         A10: ( rng s) c= ( dom f2) by A7, Lm3;

        then

         A11: ( rng (s ^\ k)) c= ( dom f2) by A9;

        now

          set t = ( |.g.| + 1);

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

          hence 0 < t;

          let n;

          

           A12: n in NAT by ORDINAL1:def 12;

          (s . (n + k)) < r by A8, NAT_1: 12;

          then ((s ^\ k) . n) < r by NAT_1:def 3;

          then ((s ^\ k) . n) in { g1 : g1 < r };

          then ((s ^\ k) . n) in ( rng (s ^\ k)) & ((s ^\ k) . n) in ( left_open_halfline r) by VALUED_0: 28, XXREAL_1: 229;

          then ((s ^\ k) . n) in (( left_open_halfline r) /\ ( dom f2)) by A11, XBOOLE_0:def 4;

          then |.(f2 . ((s ^\ k) . n)).| <= g by A4;

          then

           A13: |.((f2 /* (s ^\ k)) . n).| <= g by A10, A9, FUNCT_2: 108, XBOOLE_1: 1, A12;

          g <= |.g.| by ABSVALUE: 4;

          then g < t by Lm1;

          hence |.((f2 /* (s ^\ k)) . n).| < t by A13, XXREAL_0: 2;

        end;

        then

         A14: (f2 /* (s ^\ k)) is bounded by SEQ_2: 3;

        ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by A7, Lm3;

        then ( rng (s ^\ k)) c= (( dom f1) /\ ( dom f2)) by A7, A9;

        

        then

         A15: ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) = ((f1 (#) f2) /* (s ^\ k)) by RFUNCT_2: 8

        .= (((f1 (#) f2) /* s) ^\ k) by A7, VALUED_0: 27;

        ( rng s) c= ( dom f1) by A7, Lm3;

        then

         A16: ( rng (s ^\ k)) c= ( dom f1) by A9;

        (s ^\ k) is divergent_to-infty by A6, Th27;

        then

         A17: (f1 /* (s ^\ k)) is convergent & ( lim (f1 /* (s ^\ k))) = 0 by A1, A16, Def13;

        then

         A18: ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) is convergent by A14, SEQ_2: 25;

        hence ((f1 (#) f2) /* s) is convergent by A15, SEQ_4: 21;

        ( lim ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)))) = 0 by A17, A14, SEQ_2: 26;

        hence ( lim ((f1 (#) f2) /* s)) = 0 by A18, A15, SEQ_4: 22;

      end;

      hence (f1 (#) f2) is convergent_in-infty by A2;

      hence thesis by A5, Def13;

    end;

    theorem :: LIMFUNC1:100

    

     Th100: f1 is convergent_in+infty & f2 is convergent_in+infty & ( lim_in+infty f1) = ( lim_in+infty f2) & (for r holds ex g st r < g & g in ( dom f)) & (ex r st (((( dom f1) /\ ( right_open_halfline r)) c= (( dom f2) /\ ( right_open_halfline r)) & (( dom f) /\ ( right_open_halfline r)) c= (( dom f1) /\ ( right_open_halfline r))) or ((( dom f2) /\ ( right_open_halfline r)) c= (( dom f1) /\ ( right_open_halfline r)) & (( dom f) /\ ( right_open_halfline r)) c= (( dom f2) /\ ( right_open_halfline r)))) & for g st g in (( dom f) /\ ( right_open_halfline r)) holds (f1 . g) <= (f . g) & (f . g) <= (f2 . g)) implies f is convergent_in+infty & ( lim_in+infty f) = ( lim_in+infty f1)

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is convergent_in+infty and

       A3: ( lim_in+infty f1) = ( lim_in+infty f2) and

       A4: for r holds ex g st r < g & g in ( dom f);

      given r1 such that

       A5: (( dom f1) /\ ( right_open_halfline r1)) c= (( dom f2) /\ ( right_open_halfline r1)) & (( dom f) /\ ( right_open_halfline r1)) c= (( dom f1) /\ ( right_open_halfline r1)) or (( dom f2) /\ ( right_open_halfline r1)) c= (( dom f1) /\ ( right_open_halfline r1)) & (( dom f) /\ ( right_open_halfline r1)) c= (( dom f2) /\ ( right_open_halfline r1)) and

       A6: for g st g in (( dom f) /\ ( right_open_halfline r1)) holds (f1 . g) <= (f . g) & (f . g) <= (f2 . g);

      now

        per cases by A5;

          suppose

           A7: (( dom f1) /\ ( right_open_halfline r1)) c= (( dom f2) /\ ( right_open_halfline r1)) & (( dom f) /\ ( right_open_halfline r1)) c= (( dom f1) /\ ( right_open_halfline r1));

           A8:

          now

            let seq;

            assume that

             A9: seq is divergent_to+infty and

             A10: ( rng seq) c= ( dom f);

            consider k such that

             A11: for n st k <= n holds r1 < (seq . n) by A9;

            

             A12: (seq ^\ k) is divergent_to+infty by A9, Th26;

            now

              let x be object;

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

              then

              consider n be Element of NAT such that

               A13: x = ((seq ^\ k) . n) by FUNCT_2: 113;

              r1 < (seq . (n + k)) by A11, NAT_1: 12;

              then r1 < ((seq ^\ k) . n) by NAT_1:def 3;

              then x in { g : r1 < g } by A13;

              hence x in ( right_open_halfline r1) by XXREAL_1: 230;

            end;

            then

             A14: ( rng (seq ^\ k)) c= ( right_open_halfline r1);

            

             A15: ( rng (seq ^\ k)) c= ( rng seq) by VALUED_0: 21;

            then ( rng (seq ^\ k)) c= ( dom f) by A10;

            then

             A16: ( rng (seq ^\ k)) c= (( dom f) /\ ( right_open_halfline r1)) by A14, XBOOLE_1: 19;

            then

             A17: ( rng (seq ^\ k)) c= (( dom f1) /\ ( right_open_halfline r1)) by A7;

            then

             A18: ( rng (seq ^\ k)) c= (( dom f2) /\ ( right_open_halfline r1)) by A7;

            

             A19: (( dom f2) /\ ( right_open_halfline r1)) c= ( dom f2) by XBOOLE_1: 17;

            then ( rng (seq ^\ k)) c= ( dom f2) by A18;

            then

             A20: (f2 /* (seq ^\ k)) is convergent & ( lim (f2 /* (seq ^\ k))) = ( lim_in+infty f1) by A2, A3, A12, Def12;

            

             A21: (( dom f1) /\ ( right_open_halfline r1)) c= ( dom f1) by XBOOLE_1: 17;

            then ( rng (seq ^\ k)) c= ( dom f1) by A17;

            then

             A22: (f1 /* (seq ^\ k)) is convergent & ( lim (f1 /* (seq ^\ k))) = ( lim_in+infty f1) by A1, A12, Def12;

             A23:

            now

              let n;

              

               A24: n in NAT by ORDINAL1:def 12;

              

               A25: ((seq ^\ k) . n) in ( rng (seq ^\ k)) by VALUED_0: 28;

              then (f . ((seq ^\ k) . n)) <= (f2 . ((seq ^\ k) . n)) by A6, A16;

              then

               A26: ((f /* (seq ^\ k)) . n) <= (f2 . ((seq ^\ k) . n)) by A10, A15, FUNCT_2: 108, XBOOLE_1: 1, A24;

              (f1 . ((seq ^\ k) . n)) <= (f . ((seq ^\ k) . n)) by A6, A16, A25;

              then (f1 . ((seq ^\ k) . n)) <= ((f /* (seq ^\ k)) . n) by A10, A15, FUNCT_2: 108, A24, XBOOLE_1: 1;

              hence ((f1 /* (seq ^\ k)) . n) <= ((f /* (seq ^\ k)) . n) & ((f /* (seq ^\ k)) . n) <= ((f2 /* (seq ^\ k)) . n) by A17, A21, A18, A19, A26, FUNCT_2: 108, XBOOLE_1: 1, A24;

            end;

            

             A27: (f /* (seq ^\ k)) = ((f /* seq) ^\ k) by A10, VALUED_0: 27;

            then

             A28: ((f /* seq) ^\ k) is convergent by A22, A20, A23, SEQ_2: 19;

            hence (f /* seq) is convergent by SEQ_4: 21;

            ( lim ((f /* seq) ^\ k)) = ( lim_in+infty f1) by A22, A20, A23, A27, SEQ_2: 20;

            hence ( lim (f /* seq)) = ( lim_in+infty f1) by A28, SEQ_4: 20, SEQ_4: 21;

          end;

          hence f is convergent_in+infty by A4;

          hence thesis by A8, Def12;

        end;

          suppose

           A29: (( dom f2) /\ ( right_open_halfline r1)) c= (( dom f1) /\ ( right_open_halfline r1)) & (( dom f) /\ ( right_open_halfline r1)) c= (( dom f2) /\ ( right_open_halfline r1));

           A30:

          now

            let seq;

            assume that

             A31: seq is divergent_to+infty and

             A32: ( rng seq) c= ( dom f);

            consider k such that

             A33: for n st k <= n holds r1 < (seq . n) by A31;

            

             A34: (seq ^\ k) is divergent_to+infty by A31, Th26;

            now

              let x be object;

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

              then

              consider n be Element of NAT such that

               A35: x = ((seq ^\ k) . n) by FUNCT_2: 113;

              r1 < (seq . (n + k)) by A33, NAT_1: 12;

              then r1 < ((seq ^\ k) . n) by NAT_1:def 3;

              then x in { g : r1 < g } by A35;

              hence x in ( right_open_halfline r1) by XXREAL_1: 230;

            end;

            then

             A36: ( rng (seq ^\ k)) c= ( right_open_halfline r1);

            

             A37: ( rng (seq ^\ k)) c= ( rng seq) by VALUED_0: 21;

            then ( rng (seq ^\ k)) c= ( dom f) by A32;

            then

             A38: ( rng (seq ^\ k)) c= (( dom f) /\ ( right_open_halfline r1)) by A36, XBOOLE_1: 19;

            then

             A39: ( rng (seq ^\ k)) c= (( dom f2) /\ ( right_open_halfline r1)) by A29;

            then

             A40: ( rng (seq ^\ k)) c= (( dom f1) /\ ( right_open_halfline r1)) by A29;

            

             A41: (( dom f1) /\ ( right_open_halfline r1)) c= ( dom f1) by XBOOLE_1: 17;

            then ( rng (seq ^\ k)) c= ( dom f1) by A40;

            then

             A42: (f1 /* (seq ^\ k)) is convergent & ( lim (f1 /* (seq ^\ k))) = ( lim_in+infty f1) by A1, A34, Def12;

            

             A43: (( dom f2) /\ ( right_open_halfline r1)) c= ( dom f2) by XBOOLE_1: 17;

            then ( rng (seq ^\ k)) c= ( dom f2) by A39;

            then

             A44: (f2 /* (seq ^\ k)) is convergent & ( lim (f2 /* (seq ^\ k))) = ( lim_in+infty f1) by A2, A3, A34, Def12;

             A45:

            now

              let n;

              

               A46: n in NAT by ORDINAL1:def 12;

              

               A47: ((seq ^\ k) . n) in ( rng (seq ^\ k)) by VALUED_0: 28;

              then (f . ((seq ^\ k) . n)) <= (f2 . ((seq ^\ k) . n)) by A6, A38;

              then

               A48: ((f /* (seq ^\ k)) . n) <= (f2 . ((seq ^\ k) . n)) by A32, A37, FUNCT_2: 108, XBOOLE_1: 1, A46;

              (f1 . ((seq ^\ k) . n)) <= (f . ((seq ^\ k) . n)) by A6, A38, A47;

              then (f1 . ((seq ^\ k) . n)) <= ((f /* (seq ^\ k)) . n) by A32, A37, FUNCT_2: 108, A46, XBOOLE_1: 1;

              hence ((f1 /* (seq ^\ k)) . n) <= ((f /* (seq ^\ k)) . n) & ((f /* (seq ^\ k)) . n) <= ((f2 /* (seq ^\ k)) . n) by A39, A43, A40, A41, A48, FUNCT_2: 108, XBOOLE_1: 1, A46;

            end;

            

             A49: (f /* (seq ^\ k)) = ((f /* seq) ^\ k) by A32, VALUED_0: 27;

            then

             A50: ((f /* seq) ^\ k) is convergent by A44, A42, A45, SEQ_2: 19;

            hence (f /* seq) is convergent by SEQ_4: 21;

            ( lim ((f /* seq) ^\ k)) = ( lim_in+infty f1) by A44, A42, A45, A49, SEQ_2: 20;

            hence ( lim (f /* seq)) = ( lim_in+infty f1) by A50, SEQ_4: 20, SEQ_4: 21;

          end;

          hence f is convergent_in+infty by A4;

          hence thesis by A30, Def12;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC1:101

    f1 is convergent_in+infty & f2 is convergent_in+infty & ( lim_in+infty f1) = ( lim_in+infty f2) & (ex r st ( right_open_halfline r) c= ((( dom f1) /\ ( dom f2)) /\ ( dom f)) & for g st g in ( right_open_halfline r) holds (f1 . g) <= (f . g) & (f . g) <= (f2 . g)) implies f is convergent_in+infty & ( lim_in+infty f) = ( lim_in+infty f1)

    proof

      assume

       A1: f1 is convergent_in+infty & f2 is convergent_in+infty & ( lim_in+infty f1) = ( lim_in+infty f2);

      given r1 such that

       A2: ( right_open_halfline r1) c= ((( dom f1) /\ ( dom f2)) /\ ( dom f)) and

       A3: for g st g in ( right_open_halfline r1) holds (f1 . g) <= (f . g) & (f . g) <= (f2 . g);

      ((( dom f1) /\ ( dom f2)) /\ ( dom f)) c= ( dom f) by XBOOLE_1: 17;

      then

       A4: ( right_open_halfline r1) c= ( dom f) by A2;

       A5:

      now

        let r;

        consider g be Real such that

         A6: ( |.r.| + |.r1.|) < g by XREAL_1: 1;

        take g;

        r <= |.r.| & 0 <= |.r1.| by ABSVALUE: 4, COMPLEX1: 46;

        then (r + 0 ) <= ( |.r.| + |.r1.|) by XREAL_1: 7;

        hence r < g by A6, XXREAL_0: 2;

        r1 <= |.r1.| & 0 <= |.r.| by ABSVALUE: 4, COMPLEX1: 46;

        then ( 0 + r1) <= ( |.r.| + |.r1.|) by XREAL_1: 7;

        then r1 < g by A6, XXREAL_0: 2;

        then g in { g1 : r1 < g1 };

        then g in ( right_open_halfline r1) by XXREAL_1: 230;

        hence g in ( dom f) by A4;

      end;

      

       A7: ((( dom f1) /\ ( dom f2)) /\ ( dom f)) c= (( dom f1) /\ ( dom f2)) by XBOOLE_1: 17;

      now

        (( dom f1) /\ ( dom f2)) c= ( dom f1) by XBOOLE_1: 17;

        then ((( dom f1) /\ ( dom f2)) /\ ( dom f)) c= ( dom f1) by A7;

        then

         A8: (( dom f1) /\ ( right_open_halfline r1)) = ( right_open_halfline r1) by A2, XBOOLE_1: 1, XBOOLE_1: 28;

        (( dom f1) /\ ( dom f2)) c= ( dom f2) by XBOOLE_1: 17;

        then ((( dom f1) /\ ( dom f2)) /\ ( dom f)) c= ( dom f2) by A7;

        hence (( dom f1) /\ ( right_open_halfline r1)) c= (( dom f2) /\ ( right_open_halfline r1)) by A2, A8, XBOOLE_1: 1, XBOOLE_1: 28;

        thus (( dom f) /\ ( right_open_halfline r1)) c= (( dom f1) /\ ( right_open_halfline r1)) by A8, XBOOLE_1: 17;

        let g;

        assume g in (( dom f) /\ ( right_open_halfline r1));

        then g in ( right_open_halfline r1) by XBOOLE_0:def 4;

        hence (f1 . g) <= (f . g) & (f . g) <= (f2 . g) by A3;

      end;

      hence thesis by A1, A5, Th100;

    end;

    theorem :: LIMFUNC1:102

    

     Th102: f1 is convergent_in-infty & f2 is convergent_in-infty & ( lim_in-infty f1) = ( lim_in-infty f2) & (for r holds ex g st g < r & g in ( dom f)) & (ex r st (((( dom f1) /\ ( left_open_halfline r)) c= (( dom f2) /\ ( left_open_halfline r)) & (( dom f) /\ ( left_open_halfline r)) c= (( dom f1) /\ ( left_open_halfline r))) or ((( dom f2) /\ ( left_open_halfline r)) c= (( dom f1) /\ ( left_open_halfline r)) & (( dom f) /\ ( left_open_halfline r)) c= (( dom f2) /\ ( left_open_halfline r)))) & for g st g in (( dom f) /\ ( left_open_halfline r)) holds (f1 . g) <= (f . g) & (f . g) <= (f2 . g)) implies f is convergent_in-infty & ( lim_in-infty f) = ( lim_in-infty f1)

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is convergent_in-infty and

       A3: ( lim_in-infty f1) = ( lim_in-infty f2) and

       A4: for r holds ex g st g < r & g in ( dom f);

      given r1 such that

       A5: (( dom f1) /\ ( left_open_halfline r1)) c= (( dom f2) /\ ( left_open_halfline r1)) & (( dom f) /\ ( left_open_halfline r1)) c= (( dom f1) /\ ( left_open_halfline r1)) or (( dom f2) /\ ( left_open_halfline r1)) c= (( dom f1) /\ ( left_open_halfline r1)) & (( dom f) /\ ( left_open_halfline r1)) c= (( dom f2) /\ ( left_open_halfline r1)) and

       A6: for g st g in (( dom f) /\ ( left_open_halfline r1)) holds (f1 . g) <= (f . g) & (f . g) <= (f2 . g);

      now

        per cases by A5;

          suppose

           A7: (( dom f1) /\ ( left_open_halfline r1)) c= (( dom f2) /\ ( left_open_halfline r1)) & (( dom f) /\ ( left_open_halfline r1)) c= (( dom f1) /\ ( left_open_halfline r1));

           A8:

          now

            let seq;

            assume that

             A9: seq is divergent_to-infty and

             A10: ( rng seq) c= ( dom f);

            consider k such that

             A11: for n st k <= n holds (seq . n) < r1 by A9;

            

             A12: (seq ^\ k) is divergent_to-infty by A9, Th27;

            now

              let x be object;

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

              then

              consider n be Element of NAT such that

               A13: x = ((seq ^\ k) . n) by FUNCT_2: 113;

              (seq . (n + k)) < r1 by A11, NAT_1: 12;

              then ((seq ^\ k) . n) < r1 by NAT_1:def 3;

              then x in { g : g < r1 } by A13;

              hence x in ( left_open_halfline r1) by XXREAL_1: 229;

            end;

            then

             A14: ( rng (seq ^\ k)) c= ( left_open_halfline r1);

            

             A15: ( rng (seq ^\ k)) c= ( rng seq) by VALUED_0: 21;

            then ( rng (seq ^\ k)) c= ( dom f) by A10;

            then

             A16: ( rng (seq ^\ k)) c= (( dom f) /\ ( left_open_halfline r1)) by A14, XBOOLE_1: 19;

            then

             A17: ( rng (seq ^\ k)) c= (( dom f1) /\ ( left_open_halfline r1)) by A7;

            then

             A18: ( rng (seq ^\ k)) c= (( dom f2) /\ ( left_open_halfline r1)) by A7;

            

             A19: (( dom f2) /\ ( left_open_halfline r1)) c= ( dom f2) by XBOOLE_1: 17;

            then ( rng (seq ^\ k)) c= ( dom f2) by A18;

            then

             A20: (f2 /* (seq ^\ k)) is convergent & ( lim (f2 /* (seq ^\ k))) = ( lim_in-infty f1) by A2, A3, A12, Def13;

            

             A21: (( dom f1) /\ ( left_open_halfline r1)) c= ( dom f1) by XBOOLE_1: 17;

            then ( rng (seq ^\ k)) c= ( dom f1) by A17;

            then

             A22: (f1 /* (seq ^\ k)) is convergent & ( lim (f1 /* (seq ^\ k))) = ( lim_in-infty f1) by A1, A12, Def13;

             A23:

            now

              let n;

              

               A24: n in NAT by ORDINAL1:def 12;

              

               A25: ((seq ^\ k) . n) in ( rng (seq ^\ k)) by VALUED_0: 28;

              then (f . ((seq ^\ k) . n)) <= (f2 . ((seq ^\ k) . n)) by A6, A16;

              then

               A26: ((f /* (seq ^\ k)) . n) <= (f2 . ((seq ^\ k) . n)) by A10, A15, FUNCT_2: 108, XBOOLE_1: 1, A24;

              (f1 . ((seq ^\ k) . n)) <= (f . ((seq ^\ k) . n)) by A6, A16, A25;

              then (f1 . ((seq ^\ k) . n)) <= ((f /* (seq ^\ k)) . n) by A10, A15, FUNCT_2: 108, A24, XBOOLE_1: 1;

              hence ((f1 /* (seq ^\ k)) . n) <= ((f /* (seq ^\ k)) . n) & ((f /* (seq ^\ k)) . n) <= ((f2 /* (seq ^\ k)) . n) by A17, A21, A18, A19, A26, FUNCT_2: 108, XBOOLE_1: 1, A24;

            end;

            

             A27: (f /* (seq ^\ k)) = ((f /* seq) ^\ k) by A10, VALUED_0: 27;

            then

             A28: ((f /* seq) ^\ k) is convergent by A22, A20, A23, SEQ_2: 19;

            hence (f /* seq) is convergent by SEQ_4: 21;

            ( lim ((f /* seq) ^\ k)) = ( lim_in-infty f1) by A22, A20, A23, A27, SEQ_2: 20;

            hence ( lim (f /* seq)) = ( lim_in-infty f1) by A28, SEQ_4: 20, SEQ_4: 21;

          end;

          hence f is convergent_in-infty by A4;

          hence thesis by A8, Def13;

        end;

          suppose

           A29: (( dom f2) /\ ( left_open_halfline r1)) c= (( dom f1) /\ ( left_open_halfline r1)) & (( dom f) /\ ( left_open_halfline r1)) c= (( dom f2) /\ ( left_open_halfline r1));

           A30:

          now

            let seq;

            assume that

             A31: seq is divergent_to-infty and

             A32: ( rng seq) c= ( dom f);

            consider k such that

             A33: for n st k <= n holds (seq . n) < r1 by A31;

            

             A34: (seq ^\ k) is divergent_to-infty by A31, Th27;

            now

              let x be object;

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

              then

              consider n be Element of NAT such that

               A35: x = ((seq ^\ k) . n) by FUNCT_2: 113;

              (seq . (n + k)) < r1 by A33, NAT_1: 12;

              then ((seq ^\ k) . n) < r1 by NAT_1:def 3;

              then x in { g : g < r1 } by A35;

              hence x in ( left_open_halfline r1) by XXREAL_1: 229;

            end;

            then

             A36: ( rng (seq ^\ k)) c= ( left_open_halfline r1);

            

             A37: ( rng (seq ^\ k)) c= ( rng seq) by VALUED_0: 21;

            then ( rng (seq ^\ k)) c= ( dom f) by A32;

            then

             A38: ( rng (seq ^\ k)) c= (( dom f) /\ ( left_open_halfline r1)) by A36, XBOOLE_1: 19;

            then

             A39: ( rng (seq ^\ k)) c= (( dom f2) /\ ( left_open_halfline r1)) by A29;

            then

             A40: ( rng (seq ^\ k)) c= (( dom f1) /\ ( left_open_halfline r1)) by A29;

            

             A41: (( dom f1) /\ ( left_open_halfline r1)) c= ( dom f1) by XBOOLE_1: 17;

            then ( rng (seq ^\ k)) c= ( dom f1) by A40;

            then

             A42: (f1 /* (seq ^\ k)) is convergent & ( lim (f1 /* (seq ^\ k))) = ( lim_in-infty f1) by A1, A34, Def13;

            

             A43: (( dom f2) /\ ( left_open_halfline r1)) c= ( dom f2) by XBOOLE_1: 17;

            then ( rng (seq ^\ k)) c= ( dom f2) by A39;

            then

             A44: (f2 /* (seq ^\ k)) is convergent & ( lim (f2 /* (seq ^\ k))) = ( lim_in-infty f1) by A2, A3, A34, Def13;

             A45:

            now

              let n;

              

               A46: n in NAT by ORDINAL1:def 12;

              

               A47: ((seq ^\ k) . n) in ( rng (seq ^\ k)) by VALUED_0: 28;

              then (f . ((seq ^\ k) . n)) <= (f2 . ((seq ^\ k) . n)) by A6, A38;

              then

               A48: ((f /* (seq ^\ k)) . n) <= (f2 . ((seq ^\ k) . n)) by A32, A37, FUNCT_2: 108, XBOOLE_1: 1, A46;

              (f1 . ((seq ^\ k) . n)) <= (f . ((seq ^\ k) . n)) by A6, A38, A47;

              then (f1 . ((seq ^\ k) . n)) <= ((f /* (seq ^\ k)) . n) by A32, A37, FUNCT_2: 108, A46, XBOOLE_1: 1;

              hence ((f1 /* (seq ^\ k)) . n) <= ((f /* (seq ^\ k)) . n) & ((f /* (seq ^\ k)) . n) <= ((f2 /* (seq ^\ k)) . n) by A39, A43, A40, A41, A48, FUNCT_2: 108, XBOOLE_1: 1, A46;

            end;

            

             A49: (f /* (seq ^\ k)) = ((f /* seq) ^\ k) by A32, VALUED_0: 27;

            then

             A50: ((f /* seq) ^\ k) is convergent by A44, A42, A45, SEQ_2: 19;

            hence (f /* seq) is convergent by SEQ_4: 21;

            ( lim ((f /* seq) ^\ k)) = ( lim_in-infty f1) by A44, A42, A45, A49, SEQ_2: 20;

            hence ( lim (f /* seq)) = ( lim_in-infty f1) by A50, SEQ_4: 20, SEQ_4: 21;

          end;

          hence f is convergent_in-infty by A4;

          hence thesis by A30, Def13;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC1:103

    f1 is convergent_in-infty & f2 is convergent_in-infty & ( lim_in-infty f1) = ( lim_in-infty f2) & (ex r st ( left_open_halfline r) c= ((( dom f1) /\ ( dom f2)) /\ ( dom f)) & for g st g in ( left_open_halfline r) holds (f1 . g) <= (f . g) & (f . g) <= (f2 . g)) implies f is convergent_in-infty & ( lim_in-infty f) = ( lim_in-infty f1)

    proof

      assume

       A1: f1 is convergent_in-infty & f2 is convergent_in-infty & ( lim_in-infty f1) = ( lim_in-infty f2);

      given r1 such that

       A2: ( left_open_halfline r1) c= ((( dom f1) /\ ( dom f2)) /\ ( dom f)) and

       A3: for g st g in ( left_open_halfline r1) holds (f1 . g) <= (f . g) & (f . g) <= (f2 . g);

      ((( dom f1) /\ ( dom f2)) /\ ( dom f)) c= ( dom f) by XBOOLE_1: 17;

      then

       A4: ( left_open_halfline r1) c= ( dom f) by A2;

       A5:

      now

        let r;

        consider g be Real such that

         A6: g < (( - |.r.|) - |.r1.|) by XREAL_1: 2;

        take g;

        ( - |.r.|) <= r & 0 <= |.r1.| by ABSVALUE: 4, COMPLEX1: 46;

        then (( - |.r.|) - |.r1.|) <= (r - 0 ) by XREAL_1: 13;

        hence g < r by A6, XXREAL_0: 2;

        ( - |.r1.|) <= r1 & 0 <= |.r.| by ABSVALUE: 4, COMPLEX1: 46;

        then (( - |.r1.|) - |.r.|) <= (r1 - 0 ) by XREAL_1: 13;

        then g < r1 by A6, XXREAL_0: 2;

        then g in { g1 : g1 < r1 };

        then g in ( left_open_halfline r1) by XXREAL_1: 229;

        hence g in ( dom f) by A4;

      end;

      

       A7: ((( dom f1) /\ ( dom f2)) /\ ( dom f)) c= (( dom f1) /\ ( dom f2)) by XBOOLE_1: 17;

      now

        (( dom f1) /\ ( dom f2)) c= ( dom f1) by XBOOLE_1: 17;

        then ((( dom f1) /\ ( dom f2)) /\ ( dom f)) c= ( dom f1) by A7;

        then

         A8: (( dom f1) /\ ( left_open_halfline r1)) = ( left_open_halfline r1) by A2, XBOOLE_1: 1, XBOOLE_1: 28;

        (( dom f1) /\ ( dom f2)) c= ( dom f2) by XBOOLE_1: 17;

        then ((( dom f1) /\ ( dom f2)) /\ ( dom f)) c= ( dom f2) by A7;

        hence (( dom f1) /\ ( left_open_halfline r1)) c= (( dom f2) /\ ( left_open_halfline r1)) by A2, A8, XBOOLE_1: 1, XBOOLE_1: 28;

        thus (( dom f) /\ ( left_open_halfline r1)) c= (( dom f1) /\ ( left_open_halfline r1)) by A8, XBOOLE_1: 17;

        let g;

        assume g in (( dom f) /\ ( left_open_halfline r1));

        then g in ( left_open_halfline r1) by XBOOLE_0:def 4;

        hence (f1 . g) <= (f . g) & (f . g) <= (f2 . g) by A3;

      end;

      hence thesis by A1, A5, Th102;

    end;

    theorem :: LIMFUNC1:104

    f1 is convergent_in+infty & f2 is convergent_in+infty & (ex r st (((( dom f1) /\ ( right_open_halfline r)) c= (( dom f2) /\ ( right_open_halfline r)) & for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) <= (f2 . g)) or ((( dom f2) /\ ( right_open_halfline r)) c= (( dom f1) /\ ( right_open_halfline r)) & for g st g in (( dom f2) /\ ( right_open_halfline r)) holds (f1 . g) <= (f2 . g)))) implies ( lim_in+infty f1) <= ( lim_in+infty f2)

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is convergent_in+infty;

      given r such that

       A3: ((( dom f1) /\ ( right_open_halfline r)) c= (( dom f2) /\ ( right_open_halfline r)) & for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) <= (f2 . g)) or ((( dom f2) /\ ( right_open_halfline r)) c= (( dom f1) /\ ( right_open_halfline r)) & for g st g in (( dom f2) /\ ( right_open_halfline r)) holds (f1 . g) <= (f2 . g));

      now

        per cases by A3;

          suppose

           A4: (( dom f1) /\ ( right_open_halfline r)) c= (( dom f2) /\ ( right_open_halfline r)) & for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) <= (f2 . g);

          defpred X[ Nat, Real] means $1 < $2 & $2 in (( dom f1) /\ ( right_open_halfline r));

           A5:

          now

            let n be Element of NAT ;

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

            then

             A6: (n + 0 ) <= (n + |.r.|) by XREAL_1: 7;

            consider g such that

             A7: (n + |.r.|) < g and

             A8: g in ( dom f1) by A1;

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

            take g;

             0 <= n & r <= |.r.| by ABSVALUE: 4;

            then ( 0 + r) <= (n + |.r.|) by XREAL_1: 7;

            then r < g by A7, XXREAL_0: 2;

            then g in { g2 : r < g2 };

            then g in ( right_open_halfline r) by XXREAL_1: 230;

            hence X[n, g] by A7, A8, A6, XBOOLE_0:def 4, XXREAL_0: 2;

          end;

          consider s2 be Real_Sequence such that

           A9: for n be Element of NAT holds X[n, (s2 . n)] from FUNCT_2:sch 3( A5);

          now

            let n be Nat;

            

             A10: n in NAT by ORDINAL1:def 12;

            then n < (s2 . n) by A9;

            hence (s1 . n) <= (s2 . n) by FUNCT_1: 18, A10;

          end;

          then

           A11: s2 is divergent_to+infty by Lm5, Th20, Th42;

          

           A12: ( rng s2) c= ( dom f2)

          proof

            let x be Real;

            assume x in ( rng s2);

            then ex n be Element of NAT st x = (s2 . n) by FUNCT_2: 113;

            then x in (( dom f1) /\ ( right_open_halfline r)) by A9;

            hence thesis by A4, XBOOLE_0:def 4;

          end;

          then

           A13: ( lim (f2 /* s2)) = ( lim_in+infty f2) by A2, A11, Def12;

          

           A14: ( rng s2) c= ( dom f1)

          proof

            let x be Real;

            assume x in ( rng s2);

            then ex n be Element of NAT st x = (s2 . n) by FUNCT_2: 113;

            then x in (( dom f1) /\ ( right_open_halfline r)) by A9;

            hence thesis by XBOOLE_0:def 4;

          end;

           A15:

          now

            let n;

            

             A16: n in NAT by ORDINAL1:def 12;

            (f1 . (s2 . n)) <= (f2 . (s2 . n)) by A4, A9, A16;

            then ((f1 /* s2) . n) <= (f2 . (s2 . n)) by A14, FUNCT_2: 108, A16;

            hence ((f1 /* s2) . n) <= ((f2 /* s2) . n) by A12, FUNCT_2: 108, A16;

          end;

          

           A17: (f2 /* s2) is convergent by A2, A11, A12;

          

           A18: (f1 /* s2) is convergent by A1, A11, A14;

          ( lim (f1 /* s2)) = ( lim_in+infty f1) by A1, A11, A14, Def12;

          hence thesis by A18, A17, A13, A15, SEQ_2: 18;

        end;

          suppose

           A19: (( dom f2) /\ ( right_open_halfline r)) c= (( dom f1) /\ ( right_open_halfline r)) & for g st g in (( dom f2) /\ ( right_open_halfline r)) holds (f1 . g) <= (f2 . g);

          defpred X[ Nat, Real] means $1 < $2 & $2 in (( dom f2) /\ ( right_open_halfline r));

           A20:

          now

            let n be Element of NAT ;

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

            then

             A21: (n + 0 ) <= (n + |.r.|) by XREAL_1: 7;

            consider g such that

             A22: (n + |.r.|) < g and

             A23: g in ( dom f2) by A2;

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

            take g;

             0 <= n & r <= |.r.| by ABSVALUE: 4;

            then ( 0 + r) <= (n + |.r.|) by XREAL_1: 7;

            then r < g by A22, XXREAL_0: 2;

            then g in { g2 : r < g2 };

            then g in ( right_open_halfline r) by XXREAL_1: 230;

            hence X[n, g] by A22, A23, A21, XBOOLE_0:def 4, XXREAL_0: 2;

          end;

          consider s2 be Real_Sequence such that

           A24: for n be Element of NAT holds X[n, (s2 . n)] from FUNCT_2:sch 3( A20);

          now

            let n;

            

             A25: n in NAT by ORDINAL1:def 12;

            then n < (s2 . n) by A24;

            hence (s1 . n) <= (s2 . n) by FUNCT_1: 18, A25;

          end;

          then

           A26: s2 is divergent_to+infty by Lm5, Th20, Th42;

          

           A27: ( rng s2) c= ( dom f1)

          proof

            let x be Real;

            assume x in ( rng s2);

            then ex n be Element of NAT st x = (s2 . n) by FUNCT_2: 113;

            then x in (( dom f2) /\ ( right_open_halfline r)) by A24;

            hence thesis by A19, XBOOLE_0:def 4;

          end;

          then

           A28: ( lim (f1 /* s2)) = ( lim_in+infty f1) by A1, A26, Def12;

          

           A29: ( rng s2) c= ( dom f2)

          proof

            let x be Real;

            assume x in ( rng s2);

            then ex n be Element of NAT st x = (s2 . n) by FUNCT_2: 113;

            then x in (( dom f2) /\ ( right_open_halfline r)) by A24;

            hence thesis by XBOOLE_0:def 4;

          end;

           A30:

          now

            let n;

            

             A31: n in NAT by ORDINAL1:def 12;

            (f1 . (s2 . n)) <= (f2 . (s2 . n)) by A19, A24, A31;

            then ((f1 /* s2) . n) <= (f2 . (s2 . n)) by A27, FUNCT_2: 108, A31;

            hence ((f1 /* s2) . n) <= ((f2 /* s2) . n) by A29, FUNCT_2: 108, A31;

          end;

          

           A32: (f1 /* s2) is convergent by A1, A26, A27;

          

           A33: (f2 /* s2) is convergent by A2, A26, A29;

          ( lim (f2 /* s2)) = ( lim_in+infty f2) by A2, A26, A29, Def12;

          hence thesis by A33, A32, A28, A30, SEQ_2: 18;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC1:105

    f1 is convergent_in-infty & f2 is convergent_in-infty & (ex r st (((( dom f1) /\ ( left_open_halfline r)) c= (( dom f2) /\ ( left_open_halfline r)) & for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) <= (f2 . g)) or ((( dom f2) /\ ( left_open_halfline r)) c= (( dom f1) /\ ( left_open_halfline r)) & for g st g in (( dom f2) /\ ( left_open_halfline r)) holds (f1 . g) <= (f2 . g)))) implies ( lim_in-infty f1) <= ( lim_in-infty f2)

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is convergent_in-infty;

      given r such that

       A3: ((( dom f1) /\ ( left_open_halfline r)) c= (( dom f2) /\ ( left_open_halfline r)) & for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) <= (f2 . g)) or ((( dom f2) /\ ( left_open_halfline r)) c= (( dom f1) /\ ( left_open_halfline r)) & for g st g in (( dom f2) /\ ( left_open_halfline r)) holds (f1 . g) <= (f2 . g));

      now

        per cases by A3;

          suppose

           A4: (( dom f1) /\ ( left_open_halfline r)) c= (( dom f2) /\ ( left_open_halfline r)) & for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) <= (f2 . g);

          deffunc U( Nat) = ( - $1);

          defpred X[ Nat, Real] means $2 < ( - $1) & $2 in (( dom f1) /\ ( left_open_halfline r));

          consider s1 be Real_Sequence such that

           A5: for n holds (s1 . n) = U(n) from SEQ_1:sch 1;

           A6:

          now

            let n be Element of NAT ;

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

            then

             A7: (( - n) - |.r.|) <= (( - n) - 0 ) by XREAL_1: 13;

            consider g such that

             A8: g < (( - n) - |.r.|) and

             A9: g in ( dom f1) by A1;

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

            take g;

             0 <= n & ( - |.r.|) <= r by ABSVALUE: 4;

            then (( - |.r.|) - n) <= (r - 0 ) by XREAL_1: 13;

            then g < r by A8, XXREAL_0: 2;

            then g in { g2 : g2 < r };

            then g in ( left_open_halfline r) by XXREAL_1: 229;

            hence X[n, g] by A8, A9, A7, XBOOLE_0:def 4, XXREAL_0: 2;

          end;

          consider s2 be Real_Sequence such that

           A10: for n be Element of NAT holds X[n, (s2 . n)] from FUNCT_2:sch 3( A6);

          now

            let n;

            n in NAT by ORDINAL1:def 12;

            then (s2 . n) < ( - n) by A10;

            hence (s2 . n) <= (s1 . n) by A5;

          end;

          then

           A11: s2 is divergent_to-infty by A5, Th21, Th43;

          

           A12: ( rng s2) c= ( dom f2)

          proof

            let x be Real;

            assume x in ( rng s2);

            then ex n be Element of NAT st x = (s2 . n) by FUNCT_2: 113;

            then x in (( dom f1) /\ ( left_open_halfline r)) by A10;

            hence thesis by A4, XBOOLE_0:def 4;

          end;

          then

           A13: ( lim (f2 /* s2)) = ( lim_in-infty f2) by A2, A11, Def13;

          

           A14: ( rng s2) c= ( dom f1)

          proof

            let x be Real;

            assume x in ( rng s2);

            then ex n be Element of NAT st x = (s2 . n) by FUNCT_2: 113;

            then x in (( dom f1) /\ ( left_open_halfline r)) by A10;

            hence thesis by XBOOLE_0:def 4;

          end;

           A15:

          now

            let n;

            

             A16: n in NAT by ORDINAL1:def 12;

            (f1 . (s2 . n)) <= (f2 . (s2 . n)) by A4, A10, A16;

            then ((f1 /* s2) . n) <= (f2 . (s2 . n)) by A14, FUNCT_2: 108, A16;

            hence ((f1 /* s2) . n) <= ((f2 /* s2) . n) by A12, FUNCT_2: 108, A16;

          end;

          

           A17: (f2 /* s2) is convergent by A2, A11, A12;

          

           A18: (f1 /* s2) is convergent by A1, A11, A14;

          ( lim (f1 /* s2)) = ( lim_in-infty f1) by A1, A11, A14, Def13;

          hence thesis by A18, A17, A13, A15, SEQ_2: 18;

        end;

          suppose

           A19: (( dom f2) /\ ( left_open_halfline r)) c= (( dom f1) /\ ( left_open_halfline r)) & for g st g in (( dom f2) /\ ( left_open_halfline r)) holds (f1 . g) <= (f2 . g);

          deffunc U( Nat) = ( - $1);

          defpred X[ Nat, Real] means $2 < ( - $1) & $2 in (( dom f2) /\ ( left_open_halfline r));

          consider s1 be Real_Sequence such that

           A20: for n holds (s1 . n) = U(n) from SEQ_1:sch 1;

           A21:

          now

            let n be Element of NAT ;

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

            then

             A22: (( - n) - |.r.|) <= (( - n) - 0 ) by XREAL_1: 13;

            consider g such that

             A23: g < (( - n) - |.r.|) and

             A24: g in ( dom f2) by A2;

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

            take g;

             0 <= n & ( - |.r.|) <= r by ABSVALUE: 4;

            then (( - |.r.|) - n) <= (r - 0 ) by XREAL_1: 13;

            then g < r by A23, XXREAL_0: 2;

            then g in { g2 : g2 < r };

            then g in ( left_open_halfline r) by XXREAL_1: 229;

            hence X[n, g] by A23, A24, A22, XBOOLE_0:def 4, XXREAL_0: 2;

          end;

          consider s2 be Real_Sequence such that

           A25: for n be Element of NAT holds X[n, (s2 . n)] from FUNCT_2:sch 3( A21);

          now

            let n;

            n in NAT by ORDINAL1:def 12;

            then (s2 . n) < ( - n) by A25;

            hence (s2 . n) <= (s1 . n) by A20;

          end;

          then

           A26: s2 is divergent_to-infty by A20, Th21, Th43;

          

           A27: ( rng s2) c= ( dom f1)

          proof

            let x be Real;

            assume x in ( rng s2);

            then ex n be Element of NAT st x = (s2 . n) by FUNCT_2: 113;

            then x in (( dom f2) /\ ( left_open_halfline r)) by A25;

            hence thesis by A19, XBOOLE_0:def 4;

          end;

          then

           A28: ( lim (f1 /* s2)) = ( lim_in-infty f1) by A1, A26, Def13;

          

           A29: ( rng s2) c= ( dom f2)

          proof

            let x be Real;

            assume x in ( rng s2);

            then ex n be Element of NAT st x = (s2 . n) by FUNCT_2: 113;

            then x in (( dom f2) /\ ( left_open_halfline r)) by A25;

            hence thesis by XBOOLE_0:def 4;

          end;

           A30:

          now

            let n;

            

             A31: n in NAT by ORDINAL1:def 12;

            (f1 . (s2 . n)) <= (f2 . (s2 . n)) by A19, A25, A31;

            then ((f1 /* s2) . n) <= (f2 . (s2 . n)) by A27, FUNCT_2: 108, A31;

            hence ((f1 /* s2) . n) <= ((f2 /* s2) . n) by A29, FUNCT_2: 108, A31;

          end;

          

           A32: (f1 /* s2) is convergent by A1, A26, A27;

          

           A33: (f2 /* s2) is convergent by A2, A26, A29;

          ( lim (f2 /* s2)) = ( lim_in-infty f2) by A2, A26, A29, Def13;

          hence thesis by A33, A32, A28, A30, SEQ_2: 18;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC1:106

    (f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty) & (for r holds ex g st r < g & g in ( dom f) & (f . g) <> 0 ) implies (f ^ ) is convergent_in+infty & ( lim_in+infty (f ^ )) = 0

    proof

      assume that

       A1: f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty and

       A2: for r holds ex g st r < g & g in ( dom f) & (f . g) <> 0 ;

      

       A3: ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

       A4:

      now

        let r;

        consider g such that

         A5: r < g & g in ( dom f) and

         A6: (f . g) <> 0 by A2;

        take g;

         not (f . g) in { 0 } by A6, TARSKI:def 1;

        then not g in (f " { 0 }) by FUNCT_1:def 7;

        hence r < g & g in ( dom (f ^ )) by A3, A5, XBOOLE_0:def 5;

      end;

      now

        per cases by A1;

          suppose

           A7: f is divergent_in+infty_to+infty;

           A8:

          now

            let seq such that

             A9: seq is divergent_to+infty and

             A10: ( rng seq) c= ( dom (f ^ ));

            ( dom (f ^ )) c= ( dom f) by A3, XBOOLE_1: 36;

            then ( rng seq) c= ( dom f) by A10;

            then (f /* seq) is divergent_to+infty by A7, A9;

            then ((f /* seq) " ) is convergent & ( lim ((f /* seq) " )) = 0 by Th34;

            hence ((f ^ ) /* seq) is convergent & ( lim ((f ^ ) /* seq)) = 0 by A10, RFUNCT_2: 12;

          end;

          hence (f ^ ) is convergent_in+infty by A4;

          hence thesis by A8, Def12;

        end;

          suppose

           A11: f is divergent_in+infty_to-infty;

           A12:

          now

            let seq such that

             A13: seq is divergent_to+infty and

             A14: ( rng seq) c= ( dom (f ^ ));

            ( dom (f ^ )) c= ( dom f) by A3, XBOOLE_1: 36;

            then ( rng seq) c= ( dom f) by A14;

            then (f /* seq) is divergent_to-infty by A11, A13;

            then ((f /* seq) " ) is convergent & ( lim ((f /* seq) " )) = 0 by Th34;

            hence ((f ^ ) /* seq) is convergent & ( lim ((f ^ ) /* seq)) = 0 by A14, RFUNCT_2: 12;

          end;

          hence (f ^ ) is convergent_in+infty by A4;

          hence thesis by A12, Def12;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC1:107

    (f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty) & (for r holds ex g st g < r & g in ( dom f) & (f . g) <> 0 ) implies (f ^ ) is convergent_in-infty & ( lim_in-infty (f ^ )) = 0

    proof

      assume that

       A1: f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty and

       A2: for r holds ex g st g < r & g in ( dom f) & (f . g) <> 0 ;

      

       A3: ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

       A4:

      now

        let r;

        consider g such that

         A5: g < r & g in ( dom f) and

         A6: (f . g) <> 0 by A2;

        take g;

         not (f . g) in { 0 } by A6, TARSKI:def 1;

        then not g in (f " { 0 }) by FUNCT_1:def 7;

        hence g < r & g in ( dom (f ^ )) by A3, A5, XBOOLE_0:def 5;

      end;

      now

        per cases by A1;

          suppose

           A7: f is divergent_in-infty_to+infty;

           A8:

          now

            let seq such that

             A9: seq is divergent_to-infty and

             A10: ( rng seq) c= ( dom (f ^ ));

            ( dom (f ^ )) c= ( dom f) by A3, XBOOLE_1: 36;

            then ( rng seq) c= ( dom f) by A10;

            then (f /* seq) is divergent_to+infty by A7, A9;

            then ((f /* seq) " ) is convergent & ( lim ((f /* seq) " )) = 0 by Th34;

            hence ((f ^ ) /* seq) is convergent & ( lim ((f ^ ) /* seq)) = 0 by A10, RFUNCT_2: 12;

          end;

          hence (f ^ ) is convergent_in-infty by A4;

          hence thesis by A8, Def13;

        end;

          suppose

           A11: f is divergent_in-infty_to-infty;

           A12:

          now

            let seq such that

             A13: seq is divergent_to-infty and

             A14: ( rng seq) c= ( dom (f ^ ));

            ( dom (f ^ )) c= ( dom f) by A3, XBOOLE_1: 36;

            then ( rng seq) c= ( dom f) by A14;

            then (f /* seq) is divergent_to-infty by A11, A13;

            then ((f /* seq) " ) is convergent & ( lim ((f /* seq) " )) = 0 by Th34;

            hence ((f ^ ) /* seq) is convergent & ( lim ((f ^ ) /* seq)) = 0 by A14, RFUNCT_2: 12;

          end;

          hence (f ^ ) is convergent_in-infty by A4;

          hence thesis by A12, Def13;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC1:108

    f is convergent_in+infty & ( lim_in+infty f) = 0 & (for r holds ex g st r < g & g in ( dom f) & (f . g) <> 0 ) & (ex r st for g st g in (( dom f) /\ ( right_open_halfline r)) holds 0 <= (f . g)) implies (f ^ ) is divergent_in+infty_to+infty

    proof

      assume that

       A1: f is convergent_in+infty & ( lim_in+infty f) = 0 and

       A2: for r holds ex g st r < g & g in ( dom f) & (f . g) <> 0 ;

      given r such that

       A3: for g st g in (( dom f) /\ ( right_open_halfline r)) holds 0 <= (f . g);

      thus for r1 holds ex g1 st r1 < g1 & g1 in ( dom (f ^ ))

      proof

        let r1;

        consider g1 such that

         A4: r1 < g1 and

         A5: g1 in ( dom f) and

         A6: (f . g1) <> 0 by A2;

        take g1;

        thus r1 < g1 by A4;

         not (f . g1) in { 0 } by A6, TARSKI:def 1;

        then not g1 in (f " { 0 }) by FUNCT_1:def 7;

        then g1 in (( dom f) \ (f " { 0 })) by A5, XBOOLE_0:def 5;

        hence thesis by RFUNCT_1:def 2;

      end;

      let s be Real_Sequence;

      assume that

       A7: s is divergent_to+infty and

       A8: ( rng s) c= ( dom (f ^ ));

      consider k such that

       A9: for n st k <= n holds r < (s . n) by A7;

      

       A10: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

      ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

      then

       A11: ( dom (f ^ )) c= ( dom f) by XBOOLE_1: 36;

      then

       A12: ( rng s) c= ( dom f) by A8;

      then

       A13: ( rng (s ^\ k)) c= ( dom f) by A10;

      

       A14: (f /* (s ^\ k)) is non-zero by A8, A10, RFUNCT_2: 11, XBOOLE_1: 1;

      now

        let n;

        

         A15: n in NAT by ORDINAL1:def 12;

        r < (s . (n + k)) by A9, NAT_1: 12;

        then r < ((s ^\ k) . n) by NAT_1:def 3;

        then ((s ^\ k) . n) in { g2 : r < g2 };

        then ((s ^\ k) . n) in ( rng (s ^\ k)) & ((s ^\ k) . n) in ( right_open_halfline r) by VALUED_0: 28, XXREAL_1: 230;

        then ((s ^\ k) . n) in (( dom f) /\ ( right_open_halfline r)) by A13, XBOOLE_0:def 4;

        then

         A16: 0 <= (f . ((s ^\ k) . n)) by A3;

        ((f /* (s ^\ k)) . n) <> 0 by A14, SEQ_1: 5;

        hence 0 < ((f /* (s ^\ k)) . n) by A12, A10, A16, FUNCT_2: 108, XBOOLE_1: 1, A15;

      end;

      then

       A17: for n holds 0 <= n implies 0 < ((f /* (s ^\ k)) . n);

      (s ^\ k) is divergent_to+infty by A7, Th26;

      then (f /* (s ^\ k)) is convergent & ( lim (f /* (s ^\ k))) = 0 by A1, A13, Def12;

      then

       A18: ((f /* (s ^\ k)) " ) is divergent_to+infty by A17, Th35;

      ((f /* (s ^\ k)) " ) = (((f /* s) ^\ k) " ) by A8, A11, VALUED_0: 27, XBOOLE_1: 1

      .= (((f /* s) " ) ^\ k) by SEQM_3: 18

      .= (((f ^ ) /* s) ^\ k) by A8, RFUNCT_2: 12;

      hence thesis by A18, Th7;

    end;

    theorem :: LIMFUNC1:109

    f is convergent_in+infty & ( lim_in+infty f) = 0 & (for r holds ex g st r < g & g in ( dom f) & (f . g) <> 0 ) & (ex r st for g st g in (( dom f) /\ ( right_open_halfline r)) holds (f . g) <= 0 ) implies (f ^ ) is divergent_in+infty_to-infty

    proof

      assume that

       A1: f is convergent_in+infty & ( lim_in+infty f) = 0 and

       A2: for r holds ex g st r < g & g in ( dom f) & (f . g) <> 0 ;

      given r such that

       A3: for g st g in (( dom f) /\ ( right_open_halfline r)) holds (f . g) <= 0 ;

      thus for r1 holds ex g1 st r1 < g1 & g1 in ( dom (f ^ ))

      proof

        let r1;

        consider g1 such that

         A4: r1 < g1 and

         A5: g1 in ( dom f) and

         A6: (f . g1) <> 0 by A2;

        take g1;

        thus r1 < g1 by A4;

         not (f . g1) in { 0 } by A6, TARSKI:def 1;

        then not g1 in (f " { 0 }) by FUNCT_1:def 7;

        then g1 in (( dom f) \ (f " { 0 })) by A5, XBOOLE_0:def 5;

        hence thesis by RFUNCT_1:def 2;

      end;

      let s be Real_Sequence;

      assume that

       A7: s is divergent_to+infty and

       A8: ( rng s) c= ( dom (f ^ ));

      consider k such that

       A9: for n st k <= n holds r < (s . n) by A7;

      

       A10: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

      ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

      then

       A11: ( dom (f ^ )) c= ( dom f) by XBOOLE_1: 36;

      then

       A12: ( rng s) c= ( dom f) by A8;

      then

       A13: ( rng (s ^\ k)) c= ( dom f) by A10;

      

       A14: (f /* (s ^\ k)) is non-zero by A8, A10, RFUNCT_2: 11, XBOOLE_1: 1;

      now

        let n;

        

         A15: n in NAT by ORDINAL1:def 12;

        r < (s . (n + k)) by A9, NAT_1: 12;

        then r < ((s ^\ k) . n) by NAT_1:def 3;

        then ((s ^\ k) . n) in { g2 : r < g2 };

        then ((s ^\ k) . n) in ( rng (s ^\ k)) & ((s ^\ k) . n) in ( right_open_halfline r) by VALUED_0: 28, XXREAL_1: 230;

        then ((s ^\ k) . n) in (( dom f) /\ ( right_open_halfline r)) by A13, XBOOLE_0:def 4;

        then

         A16: (f . ((s ^\ k) . n)) <= 0 by A3;

        ((f /* (s ^\ k)) . n) <> 0 by A14, SEQ_1: 5;

        hence ((f /* (s ^\ k)) . n) < 0 by A12, A10, A16, FUNCT_2: 108, XBOOLE_1: 1, A15;

      end;

      then

       A17: for n holds 0 <= n implies ((f /* (s ^\ k)) . n) < 0 ;

      (s ^\ k) is divergent_to+infty by A7, Th26;

      then (f /* (s ^\ k)) is convergent & ( lim (f /* (s ^\ k))) = 0 by A1, A13, Def12;

      then

       A18: ((f /* (s ^\ k)) " ) is divergent_to-infty by A17, Th36;

      ((f /* (s ^\ k)) " ) = (((f /* s) ^\ k) " ) by A8, A11, VALUED_0: 27, XBOOLE_1: 1

      .= (((f /* s) " ) ^\ k) by SEQM_3: 18

      .= (((f ^ ) /* s) ^\ k) by A8, RFUNCT_2: 12;

      hence thesis by A18, Th7;

    end;

    theorem :: LIMFUNC1:110

    f is convergent_in-infty & ( lim_in-infty f) = 0 & (for r holds ex g st g < r & g in ( dom f) & (f . g) <> 0 ) & (ex r st for g st g in (( dom f) /\ ( left_open_halfline r)) holds 0 <= (f . g)) implies (f ^ ) is divergent_in-infty_to+infty

    proof

      assume that

       A1: f is convergent_in-infty & ( lim_in-infty f) = 0 and

       A2: for r holds ex g st g < r & g in ( dom f) & (f . g) <> 0 ;

      given r such that

       A3: for g st g in (( dom f) /\ ( left_open_halfline r)) holds 0 <= (f . g);

      thus for r1 holds ex g1 st g1 < r1 & g1 in ( dom (f ^ ))

      proof

        let r1;

        consider g1 such that

         A4: g1 < r1 and

         A5: g1 in ( dom f) and

         A6: (f . g1) <> 0 by A2;

        take g1;

        thus g1 < r1 by A4;

         not (f . g1) in { 0 } by A6, TARSKI:def 1;

        then not g1 in (f " { 0 }) by FUNCT_1:def 7;

        then g1 in (( dom f) \ (f " { 0 })) by A5, XBOOLE_0:def 5;

        hence thesis by RFUNCT_1:def 2;

      end;

      let s be Real_Sequence;

      assume that

       A7: s is divergent_to-infty and

       A8: ( rng s) c= ( dom (f ^ ));

      consider k such that

       A9: for n st k <= n holds (s . n) < r by A7;

      

       A10: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

      ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

      then

       A11: ( dom (f ^ )) c= ( dom f) by XBOOLE_1: 36;

      then

       A12: ( rng s) c= ( dom f) by A8;

      then

       A13: ( rng (s ^\ k)) c= ( dom f) by A10;

      

       A14: (f /* (s ^\ k)) is non-zero by A8, A10, RFUNCT_2: 11, XBOOLE_1: 1;

      now

        let n;

        

         A15: n in NAT by ORDINAL1:def 12;

        (s . (n + k)) < r by A9, NAT_1: 12;

        then ((s ^\ k) . n) < r by NAT_1:def 3;

        then ((s ^\ k) . n) in { g2 : g2 < r };

        then ((s ^\ k) . n) in ( rng (s ^\ k)) & ((s ^\ k) . n) in ( left_open_halfline r) by VALUED_0: 28, XXREAL_1: 229;

        then ((s ^\ k) . n) in (( dom f) /\ ( left_open_halfline r)) by A13, XBOOLE_0:def 4;

        then

         A16: 0 <= (f . ((s ^\ k) . n)) by A3;

         0 <> ((f /* (s ^\ k)) . n) by A14, SEQ_1: 5;

        hence 0 < ((f /* (s ^\ k)) . n) by A12, A10, A16, FUNCT_2: 108, XBOOLE_1: 1, A15;

      end;

      then

       A17: for n holds 0 <= n implies 0 < ((f /* (s ^\ k)) . n);

      (s ^\ k) is divergent_to-infty by A7, Th27;

      then (f /* (s ^\ k)) is convergent & ( lim (f /* (s ^\ k))) = 0 by A1, A13, Def13;

      then

       A18: ((f /* (s ^\ k)) " ) is divergent_to+infty by A17, Th35;

      ((f /* (s ^\ k)) " ) = (((f /* s) ^\ k) " ) by A8, A11, VALUED_0: 27, XBOOLE_1: 1

      .= (((f /* s) " ) ^\ k) by SEQM_3: 18

      .= (((f ^ ) /* s) ^\ k) by A8, RFUNCT_2: 12;

      hence thesis by A18, Th7;

    end;

    theorem :: LIMFUNC1:111

    f is convergent_in-infty & ( lim_in-infty f) = 0 & (for r holds ex g st g < r & g in ( dom f) & (f . g) <> 0 ) & (ex r st for g st g in (( dom f) /\ ( left_open_halfline r)) holds (f . g) <= 0 ) implies (f ^ ) is divergent_in-infty_to-infty

    proof

      assume that

       A1: f is convergent_in-infty & ( lim_in-infty f) = 0 and

       A2: for r holds ex g st g < r & g in ( dom f) & (f . g) <> 0 ;

      given r such that

       A3: for g st g in (( dom f) /\ ( left_open_halfline r)) holds (f . g) <= 0 ;

      thus for r1 holds ex g1 st g1 < r1 & g1 in ( dom (f ^ ))

      proof

        let r1;

        consider g1 such that

         A4: g1 < r1 and

         A5: g1 in ( dom f) and

         A6: (f . g1) <> 0 by A2;

        take g1;

        thus g1 < r1 by A4;

         not (f . g1) in { 0 } by A6, TARSKI:def 1;

        then not g1 in (f " { 0 }) by FUNCT_1:def 7;

        then g1 in (( dom f) \ (f " { 0 })) by A5, XBOOLE_0:def 5;

        hence thesis by RFUNCT_1:def 2;

      end;

      let s be Real_Sequence;

      assume that

       A7: s is divergent_to-infty and

       A8: ( rng s) c= ( dom (f ^ ));

      consider k such that

       A9: for n st k <= n holds (s . n) < r by A7;

      

       A10: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

      ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

      then

       A11: ( dom (f ^ )) c= ( dom f) by XBOOLE_1: 36;

      then

       A12: ( rng s) c= ( dom f) by A8;

      then

       A13: ( rng (s ^\ k)) c= ( dom f) by A10;

      

       A14: (f /* (s ^\ k)) is non-zero by A8, A10, RFUNCT_2: 11, XBOOLE_1: 1;

      now

        let n;

        

         A15: n in NAT by ORDINAL1:def 12;

        (s . (n + k)) < r by A9, NAT_1: 12;

        then ((s ^\ k) . n) < r by NAT_1:def 3;

        then ((s ^\ k) . n) in { g2 : g2 < r };

        then ((s ^\ k) . n) in ( rng (s ^\ k)) & ((s ^\ k) . n) in ( left_open_halfline r) by VALUED_0: 28, XXREAL_1: 229;

        then ((s ^\ k) . n) in (( dom f) /\ ( left_open_halfline r)) by A13, XBOOLE_0:def 4;

        then

         A16: (f . ((s ^\ k) . n)) <= 0 by A3;

        ((f /* (s ^\ k)) . n) <> 0 by A14, SEQ_1: 5;

        hence ((f /* (s ^\ k)) . n) < 0 by A12, A10, A16, FUNCT_2: 108, XBOOLE_1: 1, A15;

      end;

      then

       A17: for n holds 0 <= n implies ((f /* (s ^\ k)) . n) < 0 ;

      (s ^\ k) is divergent_to-infty by A7, Th27;

      then (f /* (s ^\ k)) is convergent & ( lim (f /* (s ^\ k))) = 0 by A1, A13, Def13;

      then

       A18: ((f /* (s ^\ k)) " ) is divergent_to-infty by A17, Th36;

      ((f /* (s ^\ k)) " ) = (((f /* s) ^\ k) " ) by A8, A11, VALUED_0: 27, XBOOLE_1: 1

      .= (((f /* s) " ) ^\ k) by SEQM_3: 18

      .= (((f ^ ) /* s) ^\ k) by A8, RFUNCT_2: 12;

      hence thesis by A18, Th7;

    end;

    theorem :: LIMFUNC1:112

    f is convergent_in+infty & ( lim_in+infty f) = 0 & (ex r st for g st g in (( dom f) /\ ( right_open_halfline r)) holds 0 < (f . g)) implies (f ^ ) is divergent_in+infty_to+infty

    proof

      assume that

       A1: f is convergent_in+infty and

       A2: ( lim_in+infty f) = 0 ;

      given r such that

       A3: for g st g in (( dom f) /\ ( right_open_halfline r)) holds 0 < (f . g);

      thus for r1 holds ex g1 st r1 < g1 & g1 in ( dom (f ^ ))

      proof

        let r1;

        consider g1 such that

         A4: r1 < g1 and g1 in ( dom f) by A1;

        now

          per cases ;

            suppose

             A5: g1 <= r;

            consider g2 such that

             A6: r < g2 and

             A7: g2 in ( dom f) by A1;

            take g2;

            g1 < g2 by A5, A6, XXREAL_0: 2;

            hence r1 < g2 by A4, XXREAL_0: 2;

            g2 in { r2 : r < r2 } by A6;

            then g2 in ( right_open_halfline r) by XXREAL_1: 230;

            then g2 in (( dom f) /\ ( right_open_halfline r)) by A7, XBOOLE_0:def 4;

            then 0 <> (f . g2) by A3;

            then not (f . g2) in { 0 } by TARSKI:def 1;

            then not g2 in (f " { 0 }) by FUNCT_1:def 7;

            then g2 in (( dom f) \ (f " { 0 })) by A7, XBOOLE_0:def 5;

            hence g2 in ( dom (f ^ )) by RFUNCT_1:def 2;

          end;

            suppose

             A8: r <= g1;

            consider g2 such that

             A9: g1 < g2 and

             A10: g2 in ( dom f) by A1;

            take g2;

            thus r1 < g2 by A4, A9, XXREAL_0: 2;

            r < g2 by A8, A9, XXREAL_0: 2;

            then g2 in { r2 : r < r2 };

            then g2 in ( right_open_halfline r) by XXREAL_1: 230;

            then g2 in (( dom f) /\ ( right_open_halfline r)) by A10, XBOOLE_0:def 4;

            then 0 <> (f . g2) by A3;

            then not (f . g2) in { 0 } by TARSKI:def 1;

            then not g2 in (f " { 0 }) by FUNCT_1:def 7;

            then g2 in (( dom f) \ (f " { 0 })) by A10, XBOOLE_0:def 5;

            hence g2 in ( dom (f ^ )) by RFUNCT_1:def 2;

          end;

        end;

        hence thesis;

      end;

      let s be Real_Sequence;

      assume that

       A11: s is divergent_to+infty and

       A12: ( rng s) c= ( dom (f ^ ));

      consider k such that

       A13: for n st k <= n holds r < (s . n) by A11;

      

       A14: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

      ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

      then

       A15: ( dom (f ^ )) c= ( dom f) by XBOOLE_1: 36;

      then

       A16: ( rng s) c= ( dom f) by A12;

      then

       A17: ( rng (s ^\ k)) c= ( dom f) by A14;

      now

        let n;

        

         A18: n in NAT by ORDINAL1:def 12;

        r < (s . (n + k)) by A13, NAT_1: 12;

        then r < ((s ^\ k) . n) by NAT_1:def 3;

        then ((s ^\ k) . n) in { g2 : r < g2 };

        then ((s ^\ k) . n) in ( rng (s ^\ k)) & ((s ^\ k) . n) in ( right_open_halfline r) by VALUED_0: 28, XXREAL_1: 230;

        then ((s ^\ k) . n) in (( dom f) /\ ( right_open_halfline r)) by A17, XBOOLE_0:def 4;

        then 0 < (f . ((s ^\ k) . n)) by A3;

        hence 0 < ((f /* (s ^\ k)) . n) by A16, A14, FUNCT_2: 108, XBOOLE_1: 1, A18;

      end;

      then

       A19: for n holds 0 <= n implies 0 < ((f /* (s ^\ k)) . n);

      (s ^\ k) is divergent_to+infty by A11, Th26;

      then (f /* (s ^\ k)) is convergent & ( lim (f /* (s ^\ k))) = 0 by A1, A2, A17, Def12;

      then

       A20: ((f /* (s ^\ k)) " ) is divergent_to+infty by A19, Th35;

      ((f /* (s ^\ k)) " ) = (((f /* s) ^\ k) " ) by A12, A15, VALUED_0: 27, XBOOLE_1: 1

      .= (((f /* s) " ) ^\ k) by SEQM_3: 18

      .= (((f ^ ) /* s) ^\ k) by A12, RFUNCT_2: 12;

      hence thesis by A20, Th7;

    end;

    theorem :: LIMFUNC1:113

    f is convergent_in+infty & ( lim_in+infty f) = 0 & (ex r st for g st g in (( dom f) /\ ( right_open_halfline r)) holds (f . g) < 0 ) implies (f ^ ) is divergent_in+infty_to-infty

    proof

      assume that

       A1: f is convergent_in+infty and

       A2: ( lim_in+infty f) = 0 ;

      given r such that

       A3: for g st g in (( dom f) /\ ( right_open_halfline r)) holds (f . g) < 0 ;

      thus for r1 holds ex g1 st r1 < g1 & g1 in ( dom (f ^ ))

      proof

        let r1;

        consider g1 such that

         A4: r1 < g1 and g1 in ( dom f) by A1;

        now

          per cases ;

            suppose

             A5: g1 <= r;

            consider g2 such that

             A6: r < g2 and

             A7: g2 in ( dom f) by A1;

            take g2;

            g1 < g2 by A5, A6, XXREAL_0: 2;

            hence r1 < g2 by A4, XXREAL_0: 2;

            g2 in { r2 : r < r2 } by A6;

            then g2 in ( right_open_halfline r) by XXREAL_1: 230;

            then g2 in (( dom f) /\ ( right_open_halfline r)) by A7, XBOOLE_0:def 4;

            then 0 <> (f . g2) by A3;

            then not (f . g2) in { 0 } by TARSKI:def 1;

            then not g2 in (f " { 0 }) by FUNCT_1:def 7;

            then g2 in (( dom f) \ (f " { 0 })) by A7, XBOOLE_0:def 5;

            hence g2 in ( dom (f ^ )) by RFUNCT_1:def 2;

          end;

            suppose

             A8: r <= g1;

            consider g2 such that

             A9: g1 < g2 and

             A10: g2 in ( dom f) by A1;

            take g2;

            thus r1 < g2 by A4, A9, XXREAL_0: 2;

            r < g2 by A8, A9, XXREAL_0: 2;

            then g2 in { r2 : r < r2 };

            then g2 in ( right_open_halfline r) by XXREAL_1: 230;

            then g2 in (( dom f) /\ ( right_open_halfline r)) by A10, XBOOLE_0:def 4;

            then 0 <> (f . g2) by A3;

            then not (f . g2) in { 0 } by TARSKI:def 1;

            then not g2 in (f " { 0 }) by FUNCT_1:def 7;

            then g2 in (( dom f) \ (f " { 0 })) by A10, XBOOLE_0:def 5;

            hence g2 in ( dom (f ^ )) by RFUNCT_1:def 2;

          end;

        end;

        hence thesis;

      end;

      let s be Real_Sequence;

      assume that

       A11: s is divergent_to+infty and

       A12: ( rng s) c= ( dom (f ^ ));

      consider k such that

       A13: for n st k <= n holds r < (s . n) by A11;

      

       A14: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

      ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

      then

       A15: ( dom (f ^ )) c= ( dom f) by XBOOLE_1: 36;

      then

       A16: ( rng s) c= ( dom f) by A12;

      then

       A17: ( rng (s ^\ k)) c= ( dom f) by A14;

      now

        let n;

        

         A18: n in NAT by ORDINAL1:def 12;

        r < (s . (n + k)) by A13, NAT_1: 12;

        then r < ((s ^\ k) . n) by NAT_1:def 3;

        then ((s ^\ k) . n) in { g2 : r < g2 };

        then ((s ^\ k) . n) in ( rng (s ^\ k)) & ((s ^\ k) . n) in ( right_open_halfline r) by VALUED_0: 28, XXREAL_1: 230;

        then ((s ^\ k) . n) in (( dom f) /\ ( right_open_halfline r)) by A17, XBOOLE_0:def 4;

        then (f . ((s ^\ k) . n)) < 0 by A3;

        hence ((f /* (s ^\ k)) . n) < 0 by A16, A14, FUNCT_2: 108, XBOOLE_1: 1, A18;

      end;

      then

       A19: for n holds 0 <= n implies ((f /* (s ^\ k)) . n) < 0 ;

      (s ^\ k) is divergent_to+infty by A11, Th26;

      then (f /* (s ^\ k)) is convergent & ( lim (f /* (s ^\ k))) = 0 by A1, A2, A17, Def12;

      then

       A20: ((f /* (s ^\ k)) " ) is divergent_to-infty by A19, Th36;

      ((f /* (s ^\ k)) " ) = (((f /* s) ^\ k) " ) by A12, A15, VALUED_0: 27, XBOOLE_1: 1

      .= (((f /* s) " ) ^\ k) by SEQM_3: 18

      .= (((f ^ ) /* s) ^\ k) by A12, RFUNCT_2: 12;

      hence thesis by A20, Th7;

    end;

    theorem :: LIMFUNC1:114

    f is convergent_in-infty & ( lim_in-infty f) = 0 & (ex r st for g st g in (( dom f) /\ ( left_open_halfline r)) holds 0 < (f . g)) implies (f ^ ) is divergent_in-infty_to+infty

    proof

      assume that

       A1: f is convergent_in-infty and

       A2: ( lim_in-infty f) = 0 ;

      given r such that

       A3: for g st g in (( dom f) /\ ( left_open_halfline r)) holds 0 < (f . g);

      thus for r1 holds ex g1 st g1 < r1 & g1 in ( dom (f ^ ))

      proof

        let r1;

        consider g1 such that

         A4: g1 < r1 and g1 in ( dom f) by A1;

        now

          per cases ;

            suppose

             A5: g1 <= r;

            consider g2 such that

             A6: g2 < g1 and

             A7: g2 in ( dom f) by A1;

            take g2;

            thus g2 < r1 by A4, A6, XXREAL_0: 2;

            g2 < r by A5, A6, XXREAL_0: 2;

            then g2 in { r2 : r2 < r };

            then g2 in ( left_open_halfline r) by XXREAL_1: 229;

            then g2 in (( dom f) /\ ( left_open_halfline r)) by A7, XBOOLE_0:def 4;

            then 0 <> (f . g2) by A3;

            then not (f . g2) in { 0 } by TARSKI:def 1;

            then not g2 in (f " { 0 }) by FUNCT_1:def 7;

            then g2 in (( dom f) \ (f " { 0 })) by A7, XBOOLE_0:def 5;

            hence g2 in ( dom (f ^ )) by RFUNCT_1:def 2;

          end;

            suppose

             A8: r <= g1;

            consider g2 such that

             A9: g2 < r and

             A10: g2 in ( dom f) by A1;

            take g2;

            g2 < g1 by A8, A9, XXREAL_0: 2;

            hence g2 < r1 by A4, XXREAL_0: 2;

            g2 in { r2 : r2 < r } by A9;

            then g2 in ( left_open_halfline r) by XXREAL_1: 229;

            then g2 in (( dom f) /\ ( left_open_halfline r)) by A10, XBOOLE_0:def 4;

            then 0 <> (f . g2) by A3;

            then not (f . g2) in { 0 } by TARSKI:def 1;

            then not g2 in (f " { 0 }) by FUNCT_1:def 7;

            then g2 in (( dom f) \ (f " { 0 })) by A10, XBOOLE_0:def 5;

            hence g2 in ( dom (f ^ )) by RFUNCT_1:def 2;

          end;

        end;

        hence thesis;

      end;

      let s be Real_Sequence;

      assume that

       A11: s is divergent_to-infty and

       A12: ( rng s) c= ( dom (f ^ ));

      consider k such that

       A13: for n st k <= n holds (s . n) < r by A11;

      

       A14: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

      ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

      then

       A15: ( dom (f ^ )) c= ( dom f) by XBOOLE_1: 36;

      then

       A16: ( rng s) c= ( dom f) by A12;

      then

       A17: ( rng (s ^\ k)) c= ( dom f) by A14;

      now

        let n;

        

         A18: n in NAT by ORDINAL1:def 12;

        (s . (n + k)) < r by A13, NAT_1: 12;

        then ((s ^\ k) . n) < r by NAT_1:def 3;

        then ((s ^\ k) . n) in { g2 : g2 < r };

        then ((s ^\ k) . n) in ( rng (s ^\ k)) & ((s ^\ k) . n) in ( left_open_halfline r) by VALUED_0: 28, XXREAL_1: 229;

        then ((s ^\ k) . n) in (( dom f) /\ ( left_open_halfline r)) by A17, XBOOLE_0:def 4;

        then 0 < (f . ((s ^\ k) . n)) by A3;

        hence 0 < ((f /* (s ^\ k)) . n) by A16, A14, FUNCT_2: 108, XBOOLE_1: 1, A18;

      end;

      then

       A19: for n holds 0 <= n implies 0 < ((f /* (s ^\ k)) . n);

      (s ^\ k) is divergent_to-infty by A11, Th27;

      then (f /* (s ^\ k)) is convergent & ( lim (f /* (s ^\ k))) = 0 by A1, A2, A17, Def13;

      then

       A20: ((f /* (s ^\ k)) " ) is divergent_to+infty by A19, Th35;

      ((f /* (s ^\ k)) " ) = (((f /* s) ^\ k) " ) by A12, A15, VALUED_0: 27, XBOOLE_1: 1

      .= (((f /* s) " ) ^\ k) by SEQM_3: 18

      .= (((f ^ ) /* s) ^\ k) by A12, RFUNCT_2: 12;

      hence thesis by A20, Th7;

    end;

    theorem :: LIMFUNC1:115

    f is convergent_in-infty & ( lim_in-infty f) = 0 & (ex r st for g st g in (( dom f) /\ ( left_open_halfline r)) holds (f . g) < 0 ) implies (f ^ ) is divergent_in-infty_to-infty

    proof

      assume that

       A1: f is convergent_in-infty and

       A2: ( lim_in-infty f) = 0 ;

      given r such that

       A3: for g st g in (( dom f) /\ ( left_open_halfline r)) holds (f . g) < 0 ;

      thus for r1 holds ex g1 st g1 < r1 & g1 in ( dom (f ^ ))

      proof

        let r1;

        consider g1 such that

         A4: g1 < r1 and g1 in ( dom f) by A1;

        now

          per cases ;

            suppose

             A5: g1 <= r;

            consider g2 such that

             A6: g2 < g1 and

             A7: g2 in ( dom f) by A1;

            take g2;

            thus g2 < r1 by A4, A6, XXREAL_0: 2;

            g2 < r by A5, A6, XXREAL_0: 2;

            then g2 in { r2 : r2 < r };

            then g2 in ( left_open_halfline r) by XXREAL_1: 229;

            then g2 in (( dom f) /\ ( left_open_halfline r)) by A7, XBOOLE_0:def 4;

            then 0 <> (f . g2) by A3;

            then not (f . g2) in { 0 } by TARSKI:def 1;

            then not g2 in (f " { 0 }) by FUNCT_1:def 7;

            then g2 in (( dom f) \ (f " { 0 })) by A7, XBOOLE_0:def 5;

            hence g2 in ( dom (f ^ )) by RFUNCT_1:def 2;

          end;

            suppose

             A8: r <= g1;

            consider g2 such that

             A9: g2 < r and

             A10: g2 in ( dom f) by A1;

            take g2;

            g2 < g1 by A8, A9, XXREAL_0: 2;

            hence g2 < r1 by A4, XXREAL_0: 2;

            g2 in { r2 : r2 < r } by A9;

            then g2 in ( left_open_halfline r) by XXREAL_1: 229;

            then g2 in (( dom f) /\ ( left_open_halfline r)) by A10, XBOOLE_0:def 4;

            then 0 <> (f . g2) by A3;

            then not (f . g2) in { 0 } by TARSKI:def 1;

            then not g2 in (f " { 0 }) by FUNCT_1:def 7;

            then g2 in (( dom f) \ (f " { 0 })) by A10, XBOOLE_0:def 5;

            hence g2 in ( dom (f ^ )) by RFUNCT_1:def 2;

          end;

        end;

        hence thesis;

      end;

      let s be Real_Sequence;

      assume that

       A11: s is divergent_to-infty and

       A12: ( rng s) c= ( dom (f ^ ));

      consider k such that

       A13: for n st k <= n holds (s . n) < r by A11;

      

       A14: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

      ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

      then

       A15: ( dom (f ^ )) c= ( dom f) by XBOOLE_1: 36;

      then

       A16: ( rng s) c= ( dom f) by A12;

      then

       A17: ( rng (s ^\ k)) c= ( dom f) by A14;

      now

        let n;

        

         A18: n in NAT by ORDINAL1:def 12;

        (s . (n + k)) < r by A13, NAT_1: 12;

        then ((s ^\ k) . n) < r by NAT_1:def 3;

        then ((s ^\ k) . n) in { g2 : g2 < r };

        then ((s ^\ k) . n) in ( rng (s ^\ k)) & ((s ^\ k) . n) in ( left_open_halfline r) by VALUED_0: 28, XXREAL_1: 229;

        then ((s ^\ k) . n) in (( dom f) /\ ( left_open_halfline r)) by A17, XBOOLE_0:def 4;

        then (f . ((s ^\ k) . n)) < 0 by A3;

        hence ((f /* (s ^\ k)) . n) < 0 by A16, A14, FUNCT_2: 108, XBOOLE_1: 1, A18;

      end;

      then

       A19: for n holds 0 <= n implies ((f /* (s ^\ k)) . n) < 0 ;

      (s ^\ k) is divergent_to-infty by A11, Th27;

      then (f /* (s ^\ k)) is convergent & ( lim (f /* (s ^\ k))) = 0 by A1, A2, A17, Def13;

      then

       A20: ((f /* (s ^\ k)) " ) is divergent_to-infty by A19, Th36;

      ((f /* (s ^\ k)) " ) = (((f /* s) ^\ k) " ) by A12, A15, VALUED_0: 27, XBOOLE_1: 1

      .= (((f /* s) " ) ^\ k) by SEQM_3: 18

      .= (((f ^ ) /* s) ^\ k) by A12, RFUNCT_2: 12;

      hence thesis by A20, Th7;

    end;