limfunc3.miz



    begin

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

    reserve n,k,m for Element of NAT ;

    reserve seq for Real_Sequence;

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

    

     Lm1: for g,r,r1 be Real holds 0 < g & r <= r1 implies (r - g) < r1 & r < (r1 + g)

    proof

      let g,r,r1 be Real;

      assume that

       A1: 0 < g and

       A2: r <= r1;

      (r - g) < (r1 - 0 ) by A1, A2, XREAL_1: 15;

      hence (r - g) < r1;

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

      hence thesis;

    end;

    

     Lm2: for X be set st ( rng seq) c= (( dom (f1 (#) f2)) \ X) holds ( rng seq) c= ( dom (f1 (#) f2)) & ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) & ( rng seq) c= ( dom f1) & ( rng seq) c= ( dom f2) & ( rng seq) c= (( dom f1) \ X) & ( rng seq) c= (( dom f2) \ X)

    proof

      let X be set;

      assume

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

      hence

       A2: ( rng seq) c= ( dom (f1 (#) f2)) by XBOOLE_1: 1;

      thus

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

      then

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

      ( dom (f1 (#) f2)) c= ( dom f1) by A3, XBOOLE_1: 17;

      hence ( rng seq) c= ( dom f1) & ( rng seq) c= ( dom f2) by A2, A4;

      

       A5: (( dom (f1 (#) f2)) \ X) c= (( dom f2) \ X) by A3, XBOOLE_1: 17, XBOOLE_1: 33;

      (( dom (f1 (#) f2)) \ X) c= (( dom f1) \ X) by A3, XBOOLE_1: 17, XBOOLE_1: 33;

      hence thesis by A1, A5;

    end;

    

     Lm3: (r - (1 / (n + 1))) < r & r < (r + (1 / (n + 1)))

    proof

       0 < (1 / (n + 1)) by XREAL_1: 139;

      hence thesis by Lm1;

    end;

    

     Lm4: for X be set st ( rng seq) c= (( dom (f1 + f2)) \ X) holds ( rng seq) c= ( dom (f1 + f2)) & ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) & ( rng seq) c= ( dom f1) & ( rng seq) c= ( dom f2) & ( rng seq) c= (( dom f1) \ X) & ( rng seq) c= (( dom f2) \ X)

    proof

      let X be set;

      assume

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

      hence

       A2: ( rng seq) c= ( dom (f1 + f2)) by XBOOLE_1: 1;

      thus

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

      then

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

      ( dom (f1 + f2)) c= ( dom f1) by A3, XBOOLE_1: 17;

      hence ( rng seq) c= ( dom f1) & ( rng seq) c= ( dom f2) by A2, A4;

      

       A5: (( dom (f1 + f2)) \ X) c= (( dom f2) \ X) by A3, XBOOLE_1: 17, XBOOLE_1: 33;

      (( dom (f1 + f2)) \ X) c= (( dom f1) \ X) by A3, XBOOLE_1: 17, XBOOLE_1: 33;

      hence thesis by A1, A5;

    end;

    theorem :: LIMFUNC3:1

    

     Th1: (( rng seq) c= (( dom f) /\ ( left_open_halfline x0)) or ( rng seq) c= (( dom f) /\ ( right_open_halfline x0))) implies ( rng seq) c= (( dom f) \ {x0})

    proof

      assume

       A1: ( rng seq) c= (( dom f) /\ ( left_open_halfline x0)) or ( rng seq) c= (( dom f) /\ ( right_open_halfline x0));

      let x be object;

      assume

       A2: x in ( rng seq);

      then

      consider n such that

       A3: (seq . n) = x by FUNCT_2: 113;

      now

        per cases by A1;

          suppose

           A4: ( rng seq) c= (( dom f) /\ ( left_open_halfline x0));

          then (seq . n) in ( left_open_halfline x0) by A2, A3, XBOOLE_0:def 4;

          then (seq . n) in { g1 : g1 < x0 } by XXREAL_1: 229;

          then ex g1 st g1 = (seq . n) & g1 < x0;

          then

           A5: not x in {x0} by A3, TARSKI:def 1;

          (seq . n) in ( dom f) by A2, A3, A4, XBOOLE_0:def 4;

          hence thesis by A3, A5, XBOOLE_0:def 5;

        end;

          suppose

           A6: ( rng seq) c= (( dom f) /\ ( right_open_halfline x0));

          then (seq . n) in ( right_open_halfline x0) by A2, A3, XBOOLE_0:def 4;

          then (seq . n) in { g1 : x0 < g1 } by XXREAL_1: 230;

          then ex g1 st g1 = (seq . n) & x0 < g1;

          then

           A7: not x in {x0} by A3, TARSKI:def 1;

          (seq . n) in ( dom f) by A2, A3, A6, XBOOLE_0:def 4;

          hence thesis by A3, A7, XBOOLE_0:def 5;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC3:2

    

     Th2: (for n holds 0 < |.(x0 - (seq . n)).| & |.(x0 - (seq . n)).| < (1 / (n + 1)) & (seq . n) in ( dom f)) implies seq is convergent & ( lim seq) = x0 & ( rng seq) c= ( dom f) & ( rng seq) c= (( dom f) \ {x0})

    proof

      assume

       A1: for n holds 0 < |.(x0 - (seq . n)).| & |.(x0 - (seq . n)).| < (1 / (n + 1)) & (seq . n) in ( dom f);

       A2:

      now

        let r be Real such that

         A3: 0 < r;

        consider n be Nat such that

         A4: (r " ) < n by SEQ_4: 3;

        take n;

        let k be Nat;

        assume n <= k;

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

        then

         A5: (1 / (k + 1)) <= (1 / (n + 1)) by XREAL_1: 118;

        n <= (n + 1) by NAT_1: 12;

        then (r " ) < (n + 1) by A4, XXREAL_0: 2;

        then (1 / (n + 1)) < (1 / (r " )) by A3, XREAL_1: 76;

        then (1 / (k + 1)) < (1 / (r " )) by A5, XXREAL_0: 2;

        then

         A6: (1 / (k + 1)) < r by XCMPLX_1: 216;

        k in NAT by ORDINAL1:def 12;

        then |.(x0 - (seq . k)).| < (1 / (k + 1)) by A1;

        then |.( - ((seq . k) - x0)).| < r by A6, XXREAL_0: 2;

        hence |.((seq . k) - x0).| < r by COMPLEX1: 52;

      end;

      hence seq is convergent by SEQ_2:def 6;

      hence ( lim seq) = x0 by A2, SEQ_2:def 7;

      thus

       A7: ( rng seq) c= ( dom f)

      proof

        let x be object;

        assume x in ( rng seq);

        then ex n st (seq . n) = x by FUNCT_2: 113;

        hence thesis by A1;

      end;

      let x be object;

      assume

       A8: x in ( rng seq);

      then

      consider n such that

       A9: (seq . n) = x by FUNCT_2: 113;

       0 <> |.(x0 - (seq . n)).| by A1;

      then ((x0 - (seq . n)) + (seq . n)) <> ( 0 + (seq . n)) by ABSVALUE: 2;

      then not x in {x0} by A9, TARSKI:def 1;

      hence thesis by A7, A8, XBOOLE_0:def 5;

    end;

    theorem :: LIMFUNC3:3

    

     Th3: seq is convergent & ( lim seq) = x0 & ( rng seq) c= (( dom f) \ {x0}) implies for r st 0 < r holds ex n st for k st n <= k holds 0 < |.(x0 - (seq . k)).| & |.(x0 - (seq . k)).| < r & (seq . k) in ( dom f)

    proof

      assume that

       A1: seq is convergent and

       A2: ( lim seq) = x0 and

       A3: ( rng seq) c= (( dom f) \ {x0});

      let r;

      assume 0 < r;

      then

      consider n be Nat such that

       A4: for k be Nat st n <= k holds |.((seq . k) - x0).| < r by A1, A2, SEQ_2:def 7;

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

      take n;

      let k;

      assume n <= k;

      then |.((seq . k) - x0).| < r by A4;

      then

       A5: |.( - (x0 - (seq . k))).| < r;

      now

        let n;

        (seq . n) in ( rng seq) by VALUED_0: 28;

        then not (seq . n) in {x0} by A3, XBOOLE_0:def 5;

        hence ((seq . n) - x0) <> 0 by TARSKI:def 1;

      end;

      then ((seq . k) - x0) <> 0 ;

      then 0 < |.( - (x0 - (seq . k))).| by COMPLEX1: 47;

      hence 0 < |.(x0 - (seq . k)).| by COMPLEX1: 52;

      thus |.(x0 - (seq . k)).| < r by A5, COMPLEX1: 52;

      (seq . k) in ( rng seq) by VALUED_0: 28;

      hence thesis by A3, XBOOLE_0:def 5;

    end;

    theorem :: LIMFUNC3:4

    

     Th4: 0 < r implies ( ].(x0 - r), (x0 + r).[ \ {x0}) = ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)

    proof

      assume

       A1: 0 < r;

      thus ( ].(x0 - r), (x0 + r).[ \ {x0}) c= ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)

      proof

        let x be object;

        assume

         A2: x in ( ].(x0 - r), (x0 + r).[ \ {x0});

        then

        consider r1 such that

         A3: r1 = x;

        x in ].(x0 - r), (x0 + r).[ by A2, XBOOLE_0:def 5;

        then x in { g2 : (x0 - r) < g2 & g2 < (x0 + r) } by RCOMP_1:def 2;

        then

         A4: ex g2 st g2 = x & (x0 - r) < g2 & g2 < (x0 + r);

         not x in {x0} by A2, XBOOLE_0:def 5;

        then

         A5: r1 <> x0 by A3, TARSKI:def 1;

        now

          per cases by A5, XXREAL_0: 1;

            suppose r1 < x0;

            then r1 in { g1 : (x0 - r) < g1 & g1 < x0 } by A3, A4;

            then x in ].(x0 - r), x0.[ by A3, RCOMP_1:def 2;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose x0 < r1;

            then r1 in { g1 : x0 < g1 & g1 < (x0 + r) } by A3, A4;

            then x in ].x0, (x0 + r).[ by A3, RCOMP_1:def 2;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        hence thesis;

      end;

      let x be object such that

       A6: x in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[);

      now

        per cases by A6, XBOOLE_0:def 3;

          suppose x in ].(x0 - r), x0.[;

          then x in { g1 : (x0 - r) < g1 & g1 < x0 } by RCOMP_1:def 2;

          then

          consider g1 such that

           A7: g1 = x and

           A8: (x0 - r) < g1 and

           A9: g1 < x0;

          g1 < (x0 + r) by A1, A9, Lm1;

          then x in { g2 : (x0 - r) < g2 & g2 < (x0 + r) } by A7, A8;

          then

           A10: x in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

           not x in {x0} by A7, A9, TARSKI:def 1;

          hence thesis by A10, XBOOLE_0:def 5;

        end;

          suppose x in ].x0, (x0 + r).[;

          then x in { g1 : x0 < g1 & g1 < (x0 + r) } by RCOMP_1:def 2;

          then

          consider g1 such that

           A11: g1 = x and

           A12: x0 < g1 and

           A13: g1 < (x0 + r);

          (x0 - r) < g1 by A1, A12, Lm1;

          then x in { g2 : (x0 - r) < g2 & g2 < (x0 + r) } by A11, A13;

          then

           A14: x in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

           not x in {x0} by A11, A12, TARSKI:def 1;

          hence thesis by A14, XBOOLE_0:def 5;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC3:5

    

     Th5: 0 < r2 & ( ].(x0 - r2), x0.[ \/ ].x0, (x0 + r2).[) c= ( dom f) implies for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)

    proof

      assume that

       A1: 0 < r2 and

       A2: ( ].(x0 - r2), x0.[ \/ ].x0, (x0 + r2).[) c= ( dom f);

      

       A3: ].(x0 - r2), x0.[ c= ( ].(x0 - r2), x0.[ \/ ].x0, (x0 + r2).[) by XBOOLE_1: 7;

      

       A4: ].x0, (x0 + r2).[ c= ( ].(x0 - r2), x0.[ \/ ].x0, (x0 + r2).[) by XBOOLE_1: 7;

      let r1, r2;

      assume that

       A5: r1 < x0 and

       A6: x0 < r2;

      consider g1 such that

       A7: r1 < g1 and

       A8: g1 < x0 and

       A9: g1 in ( dom f) by A1, A2, A3, A5, LIMFUNC2: 3, XBOOLE_1: 1;

      consider g2 such that

       A10: g2 < r2 and

       A11: x0 < g2 and

       A12: g2 in ( dom f) by A1, A2, A4, A6, LIMFUNC2: 4, XBOOLE_1: 1;

      take g1;

      take g2;

      thus thesis by A7, A8, A9, A10, A11, A12;

    end;

    theorem :: LIMFUNC3:6

    

     Th6: (for n holds (x0 - (1 / (n + 1))) < (seq . n) & (seq . n) < x0 & (seq . n) in ( dom f)) implies seq is convergent & ( lim seq) = x0 & ( rng seq) c= (( dom f) \ {x0})

    proof

      assume

       A1: for n holds (x0 - (1 / (n + 1))) < (seq . n) & (seq . n) < x0 & (seq . n) in ( dom f);

      

       A2: for n be Nat holds (x0 - (1 / (n + 1))) < (seq . n) & (seq . n) < x0 & (seq . n) in ( dom f)

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      hence seq is convergent & ( lim seq) = x0 by LIMFUNC2: 5;

      ( rng seq) c= (( dom f) /\ ( left_open_halfline x0)) by LIMFUNC2: 5, A2;

      hence thesis by Th1;

    end;

    theorem :: LIMFUNC3:7

    

     Th7: seq is convergent & ( lim seq) = x0 & 0 < g implies ex k st for n st k <= n holds (x0 - g) < (seq . n) & (seq . n) < (x0 + g)

    proof

      assume that

       A1: seq is convergent and

       A2: ( lim seq) = x0 and

       A3: 0 < g;

      (x0 - g) < ( lim seq) by A2, A3, Lm1;

      then

      consider k1 be Nat such that

       A4: for n be Nat st k1 <= n holds (x0 - g) < (seq . n) by A1, LIMFUNC2: 1;

      ( lim seq) < (x0 + g) by A2, A3, Lm1;

      then

      consider k2 be Nat such that

       A5: for n be Nat st k2 <= n holds (seq . n) < (x0 + g) by A1, LIMFUNC2: 2;

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

      take k;

      let n;

      assume

       A6: k <= n;

      k1 <= k by XXREAL_0: 25;

      then k1 <= n by A6, XXREAL_0: 2;

      hence (x0 - g) < (seq . n) by A4;

      k2 <= k by XXREAL_0: 25;

      then k2 <= n by A6, XXREAL_0: 2;

      hence thesis by A5;

    end;

    theorem :: LIMFUNC3:8

    

     Th8: (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) iff (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom f)) & for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom f)

    proof

      thus (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) implies (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom f)) & for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom f)

      proof

        assume

         A1: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f);

        thus for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom f)

        proof

          

           A2: x0 < (x0 + 1) by Lm1;

          let r;

          assume r < x0;

          then

          consider g1, g2 such that

           A3: r < g1 and

           A4: g1 < x0 and

           A5: g1 in ( dom f) and g2 < (x0 + 1) and x0 < g2 and g2 in ( dom f) by A1, A2;

          take g1;

          thus thesis by A3, A4, A5;

        end;

        

         A6: (x0 - 1) < x0 by Lm1;

        let r;

        assume x0 < r;

        then

        consider g1, g2 such that (x0 - 1) < g1 and g1 < x0 and g1 in ( dom f) and

         A7: g2 < r and

         A8: x0 < g2 and

         A9: g2 in ( dom f) by A1, A6;

        take g2;

        thus thesis by A7, A8, A9;

      end;

      assume that

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

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

      let r1, r2;

      assume that

       A12: r1 < x0 and

       A13: x0 < r2;

      consider g2 such that

       A14: g2 < r2 and

       A15: x0 < g2 and

       A16: g2 in ( dom f) by A11, A13;

      consider g1 such that

       A17: r1 < g1 and

       A18: g1 < x0 and

       A19: g1 in ( dom f) by A10, A12;

      take g1;

      take g2;

      thus thesis by A17, A18, A19, A14, A15, A16;

    end;

    definition

      let f, x0;

      :: LIMFUNC3:def1

      pred f is_convergent_in x0 means (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) & ex g st for seq st seq is convergent & ( lim seq) = x0 & ( rng seq) c= (( dom f) \ {x0}) holds (f /* seq) is convergent & ( lim (f /* seq)) = g;

      :: LIMFUNC3:def2

      pred f is_divergent_to+infty_in x0 means (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) & for seq st seq is convergent & ( lim seq) = x0 & ( rng seq) c= (( dom f) \ {x0}) holds (f /* seq) is divergent_to+infty;

      :: LIMFUNC3:def3

      pred f is_divergent_to-infty_in x0 means (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) & for seq st seq is convergent & ( lim seq) = x0 & ( rng seq) c= (( dom f) \ {x0}) holds (f /* seq) is divergent_to-infty;

    end

    theorem :: LIMFUNC3:9

    f is_convergent_in x0 iff (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) & ex g st for g1 st 0 < g1 holds ex g2 st 0 < g2 & for r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) holds |.((f . r1) - g).| < g1

    proof

      thus f is_convergent_in x0 implies (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) & ex g st for g1 st 0 < g1 holds ex g2 st 0 < g2 & for r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) holds |.((f . r1) - g).| < g1

      proof

        assume that

         A1: f is_convergent_in x0 and

         A2: ( not for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) or for g holds ex g1 st 0 < g1 & for g2 st 0 < g2 holds ex r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) & |.((f . r1) - g).| >= g1;

        consider g such that

         A3: for seq st seq is convergent & ( lim seq) = x0 & ( rng seq) c= (( dom f) \ {x0}) holds (f /* seq) is convergent & ( lim (f /* seq)) = g by A1;

        consider g1 such that

         A4: 0 < g1 and

         A5: for g2 st 0 < g2 holds ex r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) & |.((f . r1) - g).| >= g1 by A1, A2;

        defpred X[ Element of NAT , Real] means 0 < |.(x0 - $2).| & |.(x0 - $2).| < (1 / ($1 + 1)) & $2 in ( dom f) & |.((f . $2) - g).| >= g1;

        

         A6: for n holds ex r1 be Element of REAL st X[n, r1]

        proof

          let n;

          consider r1 such that

           A7: X[n, r1] by A5, XREAL_1: 139;

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

          take r1;

          thus thesis by A7;

        end;

        consider s be Real_Sequence such that

         A8: for n holds X[n, (s . n)] from FUNCT_2:sch 3( A6);

        

         A9: ( rng s) c= (( dom f) \ {x0}) by A8, Th2;

        

         A10: ( lim s) = x0 by A8, Th2;

        

         A11: s is convergent by A8, Th2;

        then

         A12: ( lim (f /* s)) = g by A3, A10, A9;

        (f /* s) is convergent by A3, A11, A10, A9;

        then

        consider n be Nat such that

         A13: for k be Nat st n <= k holds |.(((f /* s) . k) - g).| < g1 by A4, A12, SEQ_2:def 7;

        

         A14: |.(((f /* s) . n) - g).| < g1 by A13;

        

         A15: n in NAT by ORDINAL1:def 12;

        ( rng s) c= ( dom f) by A8, Th2;

        then |.((f . (s . n)) - g).| < g1 by A14, FUNCT_2: 108, A15;

        hence contradiction by A8, A15;

      end;

      assume

       A16: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f);

      given g such that

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

      now

        let s be Real_Sequence;

        assume that

         A18: s is convergent and

         A19: ( lim s) = x0 and

         A20: ( rng s) c= (( dom f) \ {x0});

         A21:

        now

          let g1 be Real;

          assume

           A22: 0 < g1;

          consider g2 such that

           A23: 0 < g2 and

           A24: for r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) holds |.((f . r1) - g).| < g1 by A17, A22;

          consider n such that

           A25: for k st n <= k holds 0 < |.(x0 - (s . k)).| & |.(x0 - (s . k)).| < g2 & (s . k) in ( dom f) by A18, A19, A20, A23, Th3;

          reconsider n as Nat;

          take n;

          let k be Nat;

          

           A26: k in NAT by ORDINAL1:def 12;

          assume

           A27: n <= k;

          then

           A28: |.(x0 - (s . k)).| < g2 by A25, A26;

          

           A29: (s . k) in ( dom f) by A25, A27, A26;

           0 < |.(x0 - (s . k)).| by A25, A27, A26;

          then |.((f . (s . k)) - g).| < g1 by A24, A28, A29;

          hence |.(((f /* s) . k) - g).| < g1 by A20, FUNCT_2: 108, XBOOLE_1: 1, A26;

        end;

        hence (f /* s) is convergent by SEQ_2:def 6;

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

      end;

      hence thesis by A16;

    end;

    theorem :: LIMFUNC3:10

    f is_divergent_to+infty_in x0 iff (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) & for g1 holds ex g2 st 0 < g2 & for r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) holds g1 < (f . r1)

    proof

      thus f is_divergent_to+infty_in x0 implies (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) & for g1 holds ex g2 st 0 < g2 & for r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) holds g1 < (f . r1)

      proof

        assume that

         A1: f is_divergent_to+infty_in x0 and

         A2: ( not for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) or ex g1 st for g2 st 0 < g2 holds ex r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) & (f . r1) <= g1;

        consider g1 such that

         A3: for g2 st 0 < g2 holds ex r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) & (f . r1) <= g1 by A1, A2;

        defpred X[ Element of NAT , Real] means 0 < |.(x0 - $2).| & |.(x0 - $2).| < (1 / ($1 + 1)) & $2 in ( dom f) & (f . $2) <= g1;

        

         A4: for n holds ex r1 be Element of REAL st X[n, r1]

        proof

          let n;

          consider r1 such that

           A5: X[n, r1] by A3, XREAL_1: 139;

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

          take r1;

          thus thesis by A5;

        end;

        consider s be Real_Sequence such that

         A6: for n holds X[n, (s . n)] from FUNCT_2:sch 3( A4);

        

         A7: ( rng s) c= (( dom f) \ {x0}) by A6, Th2;

        

         A8: ( lim s) = x0 by A6, Th2;

        s is convergent by A6, Th2;

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

        then

        consider n be Nat such that

         A9: for k be Nat st n <= k holds g1 < ((f /* s) . k);

        

         A10: g1 < ((f /* s) . n) by A9;

        

         A11: n in NAT by ORDINAL1:def 12;

        ( rng s) c= ( dom f) by A6, Th2;

        then g1 < (f . (s . n)) by A10, FUNCT_2: 108, A11;

        hence contradiction by A6, A11;

      end;

      assume that

       A12: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) and

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

      now

        let s be Real_Sequence;

        assume that

         A14: s is convergent and

         A15: ( lim s) = x0 and

         A16: ( rng s) c= (( dom f) \ {x0});

        now

          let g1;

          consider g2 such that

           A17: 0 < g2 and

           A18: for r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) holds g1 < (f . r1) by A13;

          consider n such that

           A19: for k st n <= k holds 0 < |.(x0 - (s . k)).| & |.(x0 - (s . k)).| < g2 & (s . k) in ( dom f) by A14, A15, A16, A17, Th3;

          reconsider n as Nat;

          take n;

          let k be Nat;

          

           A20: k in NAT by ORDINAL1:def 12;

          assume

           A21: n <= k;

          then

           A22: |.(x0 - (s . k)).| < g2 by A19, A20;

          

           A23: (s . k) in ( dom f) by A19, A21, A20;

           0 < |.(x0 - (s . k)).| by A19, A21, A20;

          then g1 < (f . (s . k)) by A18, A22, A23;

          hence g1 < ((f /* s) . k) by A16, FUNCT_2: 108, XBOOLE_1: 1, A20;

        end;

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

      end;

      hence thesis by A12;

    end;

    theorem :: LIMFUNC3:11

    f is_divergent_to-infty_in x0 iff (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) & for g1 holds ex g2 st 0 < g2 & for r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) holds (f . r1) < g1

    proof

      thus f is_divergent_to-infty_in x0 implies (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) & for g1 holds ex g2 st 0 < g2 & for r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) holds (f . r1) < g1

      proof

        assume that

         A1: f is_divergent_to-infty_in x0 and

         A2: ( not for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) or ex g1 st for g2 st 0 < g2 holds ex r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) & g1 <= (f . r1);

        consider g1 such that

         A3: for g2 st 0 < g2 holds ex r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) & g1 <= (f . r1) by A1, A2;

        defpred X[ Element of NAT , Real] means 0 < |.(x0 - $2).| & |.(x0 - $2).| < (1 / ($1 + 1)) & $2 in ( dom f) & g1 <= (f . $2);

        

         A4: for n holds ex r1 be Element of REAL st X[n, r1]

        proof

          let n;

          consider r1 such that

           A5: X[n, r1] by A3, XREAL_1: 139;

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

          take r1;

          thus thesis by A5;

        end;

        consider s be Real_Sequence such that

         A6: for n holds X[n, (s . n)] from FUNCT_2:sch 3( A4);

        

         A7: ( rng s) c= (( dom f) \ {x0}) by A6, Th2;

        

         A8: ( lim s) = x0 by A6, Th2;

        s is convergent by A6, Th2;

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

        then

        consider n be Nat such that

         A9: for k be Nat st n <= k holds ((f /* s) . k) < g1;

        

         A10: ((f /* s) . n) < g1 by A9;

        

         A11: n in NAT by ORDINAL1:def 12;

        ( rng s) c= ( dom f) by A6, Th2;

        then (f . (s . n)) < g1 by A10, FUNCT_2: 108, A11;

        hence contradiction by A6, A11;

      end;

      assume that

       A12: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) and

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

      now

        let s be Real_Sequence;

        assume that

         A14: s is convergent and

         A15: ( lim s) = x0 and

         A16: ( rng s) c= (( dom f) \ {x0});

        now

          let g1;

          consider g2 such that

           A17: 0 < g2 and

           A18: for r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) holds (f . r1) < g1 by A13;

          consider n such that

           A19: for k st n <= k holds 0 < |.(x0 - (s . k)).| & |.(x0 - (s . k)).| < g2 & (s . k) in ( dom f) by A14, A15, A16, A17, Th3;

          reconsider n as Nat;

          take n;

          let k be Nat;

          

           A20: k in NAT by ORDINAL1:def 12;

          assume

           A21: n <= k;

          then

           A22: |.(x0 - (s . k)).| < g2 by A19, A20;

          

           A23: (s . k) in ( dom f) by A19, A21, A20;

           0 < |.(x0 - (s . k)).| by A19, A21, A20;

          then (f . (s . k)) < g1 by A18, A22, A23;

          hence ((f /* s) . k) < g1 by A16, FUNCT_2: 108, XBOOLE_1: 1, A20;

        end;

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

      end;

      hence thesis by A12;

    end;

    theorem :: LIMFUNC3:12

    

     Th12: f is_divergent_to+infty_in x0 iff f is_left_divergent_to+infty_in x0 & f is_right_divergent_to+infty_in x0

    proof

      thus f is_divergent_to+infty_in x0 implies f is_left_divergent_to+infty_in x0 & f is_right_divergent_to+infty_in x0

      proof

        assume

         A1: f is_divergent_to+infty_in x0;

         A2:

        now

          let s be Real_Sequence;

          assume that

           A3: s is convergent and

           A4: ( lim s) = x0 and

           A5: ( rng s) c= (( dom f) /\ ( left_open_halfline x0));

          ( rng s) c= (( dom f) \ {x0}) by A5, Th1;

          hence (f /* s) is divergent_to+infty by A1, A3, A4;

        end;

         A6:

        now

          let s be Real_Sequence;

          assume that

           A7: s is convergent and

           A8: ( lim s) = x0 and

           A9: ( rng s) c= (( dom f) /\ ( right_open_halfline x0));

          ( rng s) c= (( dom f) \ {x0}) by A9, Th1;

          hence (f /* s) is divergent_to+infty by A1, A7, A8;

        end;

        

         A10: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) by A1;

        then for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom f) by Th8;

        hence f is_left_divergent_to+infty_in x0 by A2, LIMFUNC2:def 2;

        for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom f) by A10, Th8;

        hence thesis by A6, LIMFUNC2:def 5;

      end;

      assume that

       A11: f is_left_divergent_to+infty_in x0 and

       A12: f is_right_divergent_to+infty_in x0;

      

       A13: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom f) by A12, LIMFUNC2:def 5;

       A14:

      now

        let s be Real_Sequence such that

         A15: s is convergent and

         A16: ( lim s) = x0 and

         A17: ( rng s) c= (( dom f) \ {x0});

        now

          per cases ;

            suppose ex k st for n st k <= n holds (s . n) < x0;

            then

            consider k such that

             A18: for n st k <= n holds (s . n) < x0;

            

             A19: ( rng s) c= ( dom f) by A17, XBOOLE_1: 1;

            

             A20: ( rng (s ^\ k)) c= (( dom f) /\ ( left_open_halfline x0))

            proof

              let x be object;

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

              then

              consider n such that

               A21: ((s ^\ k) . n) = x by FUNCT_2: 113;

              (s . (n + k)) < x0 by A18, NAT_1: 12;

              then (s . (n + k)) in { g1 : g1 < x0 };

              then (s . (n + k)) in ( left_open_halfline x0) by XXREAL_1: 229;

              then

               A22: x in ( left_open_halfline x0) by A21, NAT_1:def 3;

              (s . (n + k)) in ( rng s) by VALUED_0: 28;

              then x in ( rng s) by A21, NAT_1:def 3;

              hence thesis by A19, A22, XBOOLE_0:def 4;

            end;

            

             A23: (f /* (s ^\ k)) = ((f /* s) ^\ k) by A17, VALUED_0: 27, XBOOLE_1: 1;

            ( lim (s ^\ k)) = x0 by A15, A16, SEQ_4: 20;

            then (f /* (s ^\ k)) is divergent_to+infty by A11, A15, A20, LIMFUNC2:def 2;

            hence (f /* s) is divergent_to+infty by A23, LIMFUNC1: 7;

          end;

            suppose

             A24: for k holds ex n st k <= n & (s . n) >= x0;

            now

              per cases ;

                suppose ex k st for n st k <= n holds x0 < (s . n);

                then

                consider k such that

                 A25: for n st k <= n holds (s . n) > x0;

                

                 A26: ( rng s) c= ( dom f) by A17, XBOOLE_1: 1;

                

                 A27: ( rng (s ^\ k)) c= (( dom f) /\ ( right_open_halfline x0))

                proof

                  let x be object;

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

                  then

                  consider n such that

                   A28: ((s ^\ k) . n) = x by FUNCT_2: 113;

                  x0 < (s . (n + k)) by A25, NAT_1: 12;

                  then (s . (n + k)) in { g1 : x0 < g1 };

                  then (s . (n + k)) in ( right_open_halfline x0) by XXREAL_1: 230;

                  then

                   A29: x in ( right_open_halfline x0) by A28, NAT_1:def 3;

                  (s . (n + k)) in ( rng s) by VALUED_0: 28;

                  then x in ( rng s) by A28, NAT_1:def 3;

                  hence thesis by A26, A29, XBOOLE_0:def 4;

                end;

                

                 A30: (f /* (s ^\ k)) = ((f /* s) ^\ k) by A17, VALUED_0: 27, XBOOLE_1: 1;

                ( lim (s ^\ k)) = x0 by A15, A16, SEQ_4: 20;

                then (f /* (s ^\ k)) is divergent_to+infty by A12, A15, A27, LIMFUNC2:def 5;

                hence (f /* s) is divergent_to+infty by A30, LIMFUNC1: 7;

              end;

                suppose

                 A31: for k holds ex n st k <= n & x0 >= (s . n);

                defpred X[ Nat] means (s . $1) < x0;

                 A32:

                now

                  let k;

                  consider n such that

                   A33: k <= n and

                   A34: (s . n) <= x0 by A31;

                  take n;

                  thus k <= n by A33;

                  (s . n) in ( rng s) by VALUED_0: 28;

                  then not (s . n) in {x0} by A17, XBOOLE_0:def 5;

                  then (s . n) <> x0 by TARSKI:def 1;

                  hence (s . n) < x0 by A34, XXREAL_0: 1;

                end;

                then ex m1 be Element of NAT st 0 <= m1 & (s . m1) < x0;

                then

                 A35: ex m be Nat st X[m];

                consider M be Nat such that

                 A36: X[M] & for n be Nat st X[n] holds M <= n from NAT_1:sch 5( A35);

                defpred X[ Nat] means (s . $1) > x0;

                defpred P[ set, set] means for n, m st $1 = n & $2 = m holds n < m & (s . m) < x0 & for k st n < k & (s . k) < x0 holds m <= k;

                defpred X[ Nat, set, set] means P[$2, $3];

                reconsider M9 = M as Element of NAT by ORDINAL1:def 12;

                 A37:

                now

                  let n;

                  consider m such that

                   A38: (n + 1) <= m and

                   A39: (s . m) < x0 by A32;

                  take m;

                  thus n < m & (s . m) < x0 by A38, A39, NAT_1: 13;

                end;

                

                 A40: for n be Nat holds for x be Element of NAT holds ex y be Element of NAT st X[n, x, y]

                proof

                  let n be Nat;

                  let x be Element of NAT ;

                  defpred X[ Nat] means x < $1 & (s . $1) < x0;

                  ex m st X[m] by A37;

                  then

                   A41: ex m be Nat st X[m];

                  consider l be Nat such that

                   A42: X[l] & for k be Nat st X[k] holds l <= k from NAT_1:sch 5( A41);

                  take l;

                  l in NAT by ORDINAL1:def 12;

                  hence thesis by A42;

                end;

                consider F be sequence of NAT such that

                 A43: (F . 0 ) = M9 & for n be Nat holds X[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A40);

                

                 A44: ( rng F) c= NAT by RELAT_1:def 19;

                then

                 A45: ( rng F) c= REAL by NUMBERS: 19;

                

                 A46: ( dom F) = NAT by FUNCT_2:def 1;

                then

                reconsider F as Real_Sequence by A45, RELSET_1: 4;

                 A47:

                now

                  let n;

                  (F . n) in ( rng F) by A46, FUNCT_1:def 3;

                  hence (F . n) is Element of NAT by A44;

                end;

                now

                  let n be Nat;

                  

                   A48: (F . (n + 1)) is Element of NAT by A47;

                  

                   A49: n in NAT by ORDINAL1:def 12;

                  (F . n) is Element of NAT by A47, A49;

                  hence (F . n) < (F . (n + 1)) by A43, A48;

                end;

                then

                reconsider F as increasing sequence of NAT by SEQM_3:def 6;

                

                 A50: (s * F) is subsequence of s by VALUED_0:def 17;

                then ( rng (s * F)) c= ( rng s) by VALUED_0: 21;

                then

                 A51: ( rng (s * F)) c= (( dom f) \ {x0}) by A17;

                

                 A52: for n st (s . n) < x0 holds ex m st (F . m) = n

                proof

                  defpred X[ Nat] means (s . $1) < x0 & for m holds (F . m) <> $1;

                  assume ex n st X[n];

                  then

                   A53: ex n be Nat st X[n];

                  consider M1 be Nat such that

                   A54: X[M1] & for n be Nat st X[n] holds M1 <= n from NAT_1:sch 5( A53);

                  defpred X[ Nat] means $1 < M1 & (s . $1) < x0 & ex m st (F . m) = $1;

                  

                   A55: ex n be Nat st X[n]

                  proof

                    take M;

                    

                     A56: M <> M1 by A43, A54;

                    M <= M1 by A36, A54;

                    hence M < M1 by A56, XXREAL_0: 1;

                    thus (s . M) < x0 by A36;

                    take 0 ;

                    thus thesis by A43;

                  end;

                  

                   A57: for n be Nat st X[n] holds n <= M1;

                  consider MX be Nat such that

                   A58: X[MX] & for n be Nat st X[n] holds n <= MX from NAT_1:sch 6( A57, A55);

                  

                   A59: for k st MX < k & k < M1 holds (s . k) >= x0

                  proof

                    given k such that

                     A60: MX < k and

                     A61: k < M1 and

                     A62: (s . k) < x0;

                    now

                      per cases ;

                        suppose ex m st (F . m) = k;

                        hence contradiction by A58, A60, A61, A62;

                      end;

                        suppose for m holds (F . m) <> k;

                        hence contradiction by A54, A61, A62;

                      end;

                    end;

                    hence contradiction;

                  end;

                  consider m such that

                   A63: (F . m) = MX by A58;

                  M1 in NAT by ORDINAL1:def 12;

                  then

                   A64: (F . (m + 1)) <= M1 by A43, A54, A58, A63;

                  

                   A65: (s . (F . (m + 1))) < x0 by A43, A63;

                  

                   A66: MX < (F . (m + 1)) by A43, A63;

                  now

                    assume (F . (m + 1)) <> M1;

                    then (F . (m + 1)) < M1 by A64, XXREAL_0: 1;

                    hence contradiction by A59, A66, A65;

                  end;

                  hence contradiction by A54;

                end;

                 A67:

                now

                  let k;

                  consider n such that

                   A68: k <= n and

                   A69: (s . n) >= x0 by A24;

                  take n;

                  thus k <= n by A68;

                  (s . n) in ( rng s) by VALUED_0: 28;

                  then not (s . n) in {x0} by A17, XBOOLE_0:def 5;

                  then (s . n) <> x0 by TARSKI:def 1;

                  hence (s . n) > x0 by A69, XXREAL_0: 1;

                end;

                then ex mn be Element of NAT st 0 <= mn & (s . mn) > x0;

                then

                 A70: ex m be Nat st X[m];

                consider N be Nat such that

                 A71: X[N] & for n be Nat st X[n] holds N <= n from NAT_1:sch 5( A70);

                defpred X[ Nat] means ((s * F) . $1) < x0;

                

                 A72: for k be Nat st X[k] holds X[(k + 1)]

                proof

                  let k be Nat such that ((s * F) . k) < x0;

                   P[(F . k), (F . (k + 1))] by A43;

                  then (s . (F . (k + 1))) < x0;

                  hence thesis by FUNCT_2: 15;

                end;

                

                 A73: X[ 0 ] by A36, A43, FUNCT_2: 15;

                

                 A74: for k be Nat holds X[k] from NAT_1:sch 2( A73, A72);

                

                 A75: ( rng (s * F)) c= (( dom f) /\ ( left_open_halfline x0))

                proof

                  let x be object;

                  assume

                   A76: x in ( rng (s * F));

                  then

                  consider n such that

                   A77: ((s * F) . n) = x by FUNCT_2: 113;

                  ((s * F) . n) < x0 by A74;

                  then x in { g1 : g1 < x0 } by A77;

                  then

                   A78: x in ( left_open_halfline x0) by XXREAL_1: 229;

                  x in ( dom f) by A51, A76, XBOOLE_0:def 5;

                  hence thesis by A78, XBOOLE_0:def 4;

                end;

                defpred P[ set, set] means for n, m st $1 = n & $2 = m holds n < m & (s . m) > x0 & for k st n < k & (s . k) > x0 holds m <= k;

                defpred X[ Nat, set, set] means P[$2, $3];

                

                 A79: (s * F) is convergent by A15, A50, SEQ_4: 16;

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

                 A80:

                now

                  let n;

                  consider m such that

                   A81: (n + 1) <= m and

                   A82: (s . m) > x0 by A67;

                  take m;

                  thus n < m & (s . m) > x0 by A81, A82, NAT_1: 13;

                end;

                

                 A83: for n be Nat holds for x be Element of NAT holds ex y be Element of NAT st X[n, x, y]

                proof

                  let n be Nat;

                  let x be Element of NAT ;

                  defpred X[ Nat] means x < $1 & (s . $1) > x0;

                  ex m st X[m] by A80;

                  then

                   A84: ex m be Nat st X[m];

                  consider l be Nat such that

                   A85: X[l] & for k be Nat st X[k] holds l <= k from NAT_1:sch 5( A84);

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

                  take l;

                  thus thesis by A85;

                end;

                consider G be sequence of NAT such that

                 A86: (G . 0 ) = N9 & for n be Nat holds X[n, (G . n), (G . (n + 1))] from RECDEF_1:sch 2( A83);

                

                 A87: ( rng G) c= NAT by RELAT_1:def 19;

                then

                 A88: ( rng G) c= REAL by NUMBERS: 19;

                

                 A89: ( dom G) = NAT by FUNCT_2:def 1;

                then

                reconsider G as Real_Sequence by A88, RELSET_1: 4;

                 A90:

                now

                  let n;

                  (G . n) in ( rng G) by A89, FUNCT_1:def 3;

                  hence (G . n) is Element of NAT by A87;

                end;

                now

                  let n be Nat;

                  

                   A91: n in NAT by ORDINAL1:def 12;

                  

                   A92: (G . (n + 1)) is Element of NAT by A90;

                  (G . n) is Element of NAT by A90, A91;

                  hence (G . n) < (G . (n + 1)) by A86, A92;

                end;

                then

                reconsider G as increasing sequence of NAT by SEQM_3:def 6;

                

                 A93: (s * G) is subsequence of s by VALUED_0:def 17;

                then ( rng (s * G)) c= ( rng s) by VALUED_0: 21;

                then

                 A94: ( rng (s * G)) c= (( dom f) \ {x0}) by A17;

                defpred X[ Nat] means (s . $1) > x0 & for m holds (G . m) <> $1;

                

                 A95: for n st (s . n) > x0 holds ex m st (G . m) = n

                proof

                  assume ex n st X[n];

                  then

                   A96: ex n be Nat st X[n];

                  consider N1 be Nat such that

                   A97: X[N1] & for n be Nat st X[n] holds N1 <= n from NAT_1:sch 5( A96);

                  defpred X[ Nat] means $1 < N1 & (s . $1) > x0 & ex m st (G . m) = $1;

                  

                   A98: ex n be Nat st X[n]

                  proof

                    take N;

                    

                     A99: N <> N1 by A86, A97;

                    N <= N1 by A71, A97;

                    hence N < N1 by A99, XXREAL_0: 1;

                    thus (s . N) > x0 by A71;

                    take 0 ;

                    thus thesis by A86;

                  end;

                  

                   A100: for n be Nat st X[n] holds n <= N1;

                  consider NX be Nat such that

                   A101: X[NX] & for n be Nat st X[n] holds n <= NX from NAT_1:sch 6( A100, A98);

                  

                   A102: for k st NX < k & k < N1 holds (s . k) <= x0

                  proof

                    given k such that

                     A103: NX < k and

                     A104: k < N1 and

                     A105: (s . k) > x0;

                    now

                      per cases ;

                        suppose ex m st (G . m) = k;

                        hence contradiction by A101, A103, A104, A105;

                      end;

                        suppose for m holds (G . m) <> k;

                        hence contradiction by A97, A104, A105;

                      end;

                    end;

                    hence contradiction;

                  end;

                  consider m such that

                   A106: (G . m) = NX by A101;

                  N1 in NAT by ORDINAL1:def 12;

                  then

                   A107: (G . (m + 1)) <= N1 by A86, A97, A101, A106;

                  

                   A108: (s . (G . (m + 1))) > x0 by A86, A106;

                  

                   A109: NX < (G . (m + 1)) by A86, A106;

                  now

                    assume (G . (m + 1)) <> N1;

                    then (G . (m + 1)) < N1 by A107, XXREAL_0: 1;

                    hence contradiction by A102, A109, A108;

                  end;

                  hence contradiction by A97;

                end;

                defpred X[ Nat] means ((s * G) . $1) > x0;

                

                 A110: for k be Nat st X[k] holds X[(k + 1)]

                proof

                  let k be Nat such that ((s * G) . k) > x0;

                   P[(G . k), (G . (k + 1))] by A86;

                  then (s . (G . (k + 1))) > x0;

                  hence thesis by FUNCT_2: 15;

                end;

                

                 A111: X[ 0 ] by A71, A86, FUNCT_2: 15;

                

                 A112: for k be Nat holds X[k] from NAT_1:sch 2( A111, A110);

                

                 A113: ( rng (s * G)) c= (( dom f) /\ ( right_open_halfline x0))

                proof

                  let x be object;

                  assume

                   A114: x in ( rng (s * G));

                  then

                  consider n such that

                   A115: ((s * G) . n) = x by FUNCT_2: 113;

                  ((s * G) . n) > x0 by A112;

                  then x in { g1 : x0 < g1 } by A115;

                  then

                   A116: x in ( right_open_halfline x0) by XXREAL_1: 230;

                  x in ( dom f) by A94, A114, XBOOLE_0:def 5;

                  hence thesis by A116, XBOOLE_0:def 4;

                end;

                

                 A117: (s * G) is convergent by A15, A93, SEQ_4: 16;

                ( lim (s * G)) = x0 by A15, A16, A93, SEQ_4: 17;

                then

                 A118: (f /* (s * G)) is divergent_to+infty by A12, A117, A113, LIMFUNC2:def 5;

                ( lim (s * F)) = x0 by A15, A16, A50, SEQ_4: 17;

                then

                 A119: (f /* (s * F)) is divergent_to+infty by A11, A79, A75, LIMFUNC2:def 2;

                now

                  let r;

                  consider n1 be Nat such that

                   A120: for k be Nat st n1 <= k holds r < ((f /* (s * F)) . k) by A119;

                  consider n2 be Nat such that

                   A121: for k be Nat st n2 <= k holds r < ((f /* (s * G)) . k) by A118;

                  reconsider n = ( max ((F . n1),(G . n2))) as Nat;

                  take n;

                  let k be Nat;

                  

                   A122: k in NAT by ORDINAL1:def 12;

                  assume

                   A123: n <= k;

                  (s . k) in ( rng s) by VALUED_0: 28;

                  then not (s . k) in {x0} by A17, XBOOLE_0:def 5;

                  then

                   A124: (s . k) <> x0 by TARSKI:def 1;

                  now

                    per cases by A124, XXREAL_0: 1;

                      suppose (s . k) < x0;

                      then

                      consider l be Element of NAT such that

                       A125: k = (F . l) by A52, A122;

                      (F . n1) <= n by XXREAL_0: 25;

                      then (F . n1) <= k by A123, XXREAL_0: 2;

                      then l >= n1 by A125, SEQM_3: 1;

                      then r < ((f /* (s * F)) . l) by A120;

                      then r < (f . ((s * F) . l)) by A51, FUNCT_2: 108, XBOOLE_1: 1;

                      then r < (f . (s . k)) by A125, FUNCT_2: 15;

                      hence r < ((f /* s) . k) by A17, FUNCT_2: 108, XBOOLE_1: 1, A122;

                    end;

                      suppose (s . k) > x0;

                      then

                      consider l be Element of NAT such that

                       A126: k = (G . l) by A95, A122;

                      (G . n2) <= n by XXREAL_0: 25;

                      then (G . n2) <= k by A123, XXREAL_0: 2;

                      then l >= n2 by A126, SEQM_3: 1;

                      then r < ((f /* (s * G)) . l) by A121;

                      then r < (f . ((s * G) . l)) by A94, FUNCT_2: 108, XBOOLE_1: 1;

                      then r < (f . (s . k)) by A126, FUNCT_2: 15;

                      hence r < ((f /* s) . k) by A17, FUNCT_2: 108, XBOOLE_1: 1, A122;

                    end;

                  end;

                  hence r < ((f /* s) . k);

                end;

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

              end;

            end;

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

          end;

        end;

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

      end;

      for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom f) by A11, LIMFUNC2:def 2;

      then for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) by A13, Th8;

      hence thesis by A14;

    end;

    theorem :: LIMFUNC3:13

    

     Th13: f is_divergent_to-infty_in x0 iff f is_left_divergent_to-infty_in x0 & f is_right_divergent_to-infty_in x0

    proof

      thus f is_divergent_to-infty_in x0 implies f is_left_divergent_to-infty_in x0 & f is_right_divergent_to-infty_in x0

      proof

        assume

         A1: f is_divergent_to-infty_in x0;

         A2:

        now

          let s be Real_Sequence;

          assume that

           A3: s is convergent and

           A4: ( lim s) = x0 and

           A5: ( rng s) c= (( dom f) /\ ( left_open_halfline x0));

          ( rng s) c= (( dom f) \ {x0}) by A5, Th1;

          hence (f /* s) is divergent_to-infty by A1, A3, A4;

        end;

         A6:

        now

          let s be Real_Sequence;

          assume that

           A7: s is convergent and

           A8: ( lim s) = x0 and

           A9: ( rng s) c= (( dom f) /\ ( right_open_halfline x0));

          ( rng s) c= (( dom f) \ {x0}) by A9, Th1;

          hence (f /* s) is divergent_to-infty by A1, A7, A8;

        end;

        

         A10: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) by A1;

        then for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom f) by Th8;

        hence f is_left_divergent_to-infty_in x0 by A2, LIMFUNC2:def 3;

        for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom f) by A10, Th8;

        hence thesis by A6, LIMFUNC2:def 6;

      end;

      assume that

       A11: f is_left_divergent_to-infty_in x0 and

       A12: f is_right_divergent_to-infty_in x0;

       A13:

      now

        let s be Real_Sequence such that

         A14: s is convergent and

         A15: ( lim s) = x0 and

         A16: ( rng s) c= (( dom f) \ {x0});

        now

          per cases ;

            suppose ex k st for n st k <= n holds (s . n) < x0;

            then

            consider k such that

             A17: for n st k <= n holds (s . n) < x0;

            

             A18: ( rng s) c= ( dom f) by A16, XBOOLE_1: 1;

            

             A19: ( rng (s ^\ k)) c= (( dom f) /\ ( left_open_halfline x0))

            proof

              let x be object;

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

              then

              consider n such that

               A20: ((s ^\ k) . n) = x by FUNCT_2: 113;

              (s . (n + k)) < x0 by A17, NAT_1: 12;

              then (s . (n + k)) in { g1 : g1 < x0 };

              then (s . (n + k)) in ( left_open_halfline x0) by XXREAL_1: 229;

              then

               A21: x in ( left_open_halfline x0) by A20, NAT_1:def 3;

              (s . (n + k)) in ( rng s) by VALUED_0: 28;

              then x in ( rng s) by A20, NAT_1:def 3;

              hence thesis by A18, A21, XBOOLE_0:def 4;

            end;

            

             A22: (f /* (s ^\ k)) = ((f /* s) ^\ k) by A16, VALUED_0: 27, XBOOLE_1: 1;

            ( lim (s ^\ k)) = x0 by A14, A15, SEQ_4: 20;

            then (f /* (s ^\ k)) is divergent_to-infty by A11, A14, A19, LIMFUNC2:def 3;

            hence (f /* s) is divergent_to-infty by A22, LIMFUNC1: 7;

          end;

            suppose

             A23: for k holds ex n st k <= n & (s . n) >= x0;

            now

              per cases ;

                suppose ex k st for n st k <= n holds x0 < (s . n);

                then

                consider k such that

                 A24: for n st k <= n holds (s . n) > x0;

                

                 A25: ( rng s) c= ( dom f) by A16, XBOOLE_1: 1;

                

                 A26: ( rng (s ^\ k)) c= (( dom f) /\ ( right_open_halfline x0))

                proof

                  let x be object;

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

                  then

                  consider n such that

                   A27: ((s ^\ k) . n) = x by FUNCT_2: 113;

                  x0 < (s . (n + k)) by A24, NAT_1: 12;

                  then (s . (n + k)) in { g1 : x0 < g1 };

                  then (s . (n + k)) in ( right_open_halfline x0) by XXREAL_1: 230;

                  then

                   A28: x in ( right_open_halfline x0) by A27, NAT_1:def 3;

                  (s . (n + k)) in ( rng s) by VALUED_0: 28;

                  then x in ( rng s) by A27, NAT_1:def 3;

                  hence thesis by A25, A28, XBOOLE_0:def 4;

                end;

                

                 A29: (f /* (s ^\ k)) = ((f /* s) ^\ k) by A16, VALUED_0: 27, XBOOLE_1: 1;

                ( lim (s ^\ k)) = x0 by A14, A15, SEQ_4: 20;

                then (f /* (s ^\ k)) is divergent_to-infty by A12, A14, A26, LIMFUNC2:def 6;

                hence (f /* s) is divergent_to-infty by A29, LIMFUNC1: 7;

              end;

                suppose

                 A30: for k holds ex n st k <= n & x0 >= (s . n);

                defpred P[ set, set] means for n, m st $1 = n & $2 = m holds n < m & (s . m) < x0 & for k st n < k & (s . k) < x0 holds m <= k;

                defpred X[ Nat, set, set] means P[$2, $3];

                defpred X[ Nat] means (s . $1) < x0;

                 A31:

                now

                  let k;

                  consider n such that

                   A32: k <= n and

                   A33: (s . n) <= x0 by A30;

                  take n;

                  thus k <= n by A32;

                  (s . n) in ( rng s) by VALUED_0: 28;

                  then not (s . n) in {x0} by A16, XBOOLE_0:def 5;

                  then (s . n) <> x0 by TARSKI:def 1;

                  hence (s . n) < x0 by A33, XXREAL_0: 1;

                end;

                then ex m1 be Element of NAT st 0 <= m1 & (s . m1) < x0;

                then

                 A34: ex m be Nat st X[m];

                consider M be Nat such that

                 A35: X[M] & for n be Nat st X[n] holds M <= n from NAT_1:sch 5( A34);

                reconsider M9 = M as Element of NAT by ORDINAL1:def 12;

                 A36:

                now

                  let n;

                  consider m such that

                   A37: (n + 1) <= m and

                   A38: (s . m) < x0 by A31;

                  take m;

                  thus n < m & (s . m) < x0 by A37, A38, NAT_1: 13;

                end;

                

                 A39: for n be Nat holds for x be Element of NAT holds ex y be Element of NAT st X[n, x, y]

                proof

                  let n be Nat;

                  let x be Element of NAT ;

                  defpred X[ Nat] means x < $1 & (s . $1) < x0;

                  ex m st X[m] by A36;

                  then

                   A40: ex m be Nat st X[m];

                  consider l be Nat such that

                   A41: X[l] & for k be Nat st X[k] holds l <= k from NAT_1:sch 5( A40);

                  take l;

                  l in NAT by ORDINAL1:def 12;

                  hence thesis by A41;

                end;

                consider F be sequence of NAT such that

                 A42: (F . 0 ) = M9 & for n be Nat holds X[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A39);

                

                 A43: ( rng F) c= NAT by RELAT_1:def 19;

                then

                 A44: ( rng F) c= REAL by NUMBERS: 19;

                

                 A45: ( dom F) = NAT by FUNCT_2:def 1;

                then

                reconsider F as Real_Sequence by A44, RELSET_1: 4;

                 A46:

                now

                  let n;

                  (F . n) in ( rng F) by A45, FUNCT_1:def 3;

                  hence (F . n) is Element of NAT by A43;

                end;

                now

                  let n be Nat;

                  

                   A47: n in NAT by ORDINAL1:def 12;

                  

                   A48: (F . (n + 1)) is Element of NAT by A46;

                  (F . n) is Element of NAT by A46, A47;

                  hence (F . n) < (F . (n + 1)) by A42, A48;

                end;

                then

                reconsider F as increasing sequence of NAT by SEQM_3:def 6;

                

                 A49: (s * F) is subsequence of s by VALUED_0:def 17;

                then ( rng (s * F)) c= ( rng s) by VALUED_0: 21;

                then

                 A50: ( rng (s * F)) c= (( dom f) \ {x0}) by A16;

                defpred X[ Nat] means (s . $1) < x0 & for m holds (F . m) <> $1;

                

                 A51: for n st (s . n) < x0 holds ex m st (F . m) = n

                proof

                  assume ex n st X[n];

                  then

                   A52: ex n be Nat st X[n];

                  consider M1 be Nat such that

                   A53: X[M1] & for n be Nat st X[n] holds M1 <= n from NAT_1:sch 5( A52);

                  defpred X[ Nat] means $1 < M1 & (s . $1) < x0 & ex m st (F . m) = $1;

                  

                   A54: ex n be Nat st X[n]

                  proof

                    take M;

                    

                     A55: M <> M1 by A42, A53;

                    M <= M1 by A35, A53;

                    hence M < M1 by A55, XXREAL_0: 1;

                    thus (s . M) < x0 by A35;

                    take 0 ;

                    thus thesis by A42;

                  end;

                  

                   A56: for n be Nat st X[n] holds n <= M1;

                  consider MX be Nat such that

                   A57: X[MX] & for n be Nat st X[n] holds n <= MX from NAT_1:sch 6( A56, A54);

                  

                   A58: for k st MX < k & k < M1 holds (s . k) >= x0

                  proof

                    given k such that

                     A59: MX < k and

                     A60: k < M1 and

                     A61: (s . k) < x0;

                    now

                      per cases ;

                        suppose ex m st (F . m) = k;

                        hence contradiction by A57, A59, A60, A61;

                      end;

                        suppose for m holds (F . m) <> k;

                        hence contradiction by A53, A60, A61;

                      end;

                    end;

                    hence contradiction;

                  end;

                  consider m such that

                   A62: (F . m) = MX by A57;

                  M1 in NAT by ORDINAL1:def 12;

                  then

                   A63: (F . (m + 1)) <= M1 by A42, A53, A57, A62;

                  

                   A64: (s . (F . (m + 1))) < x0 by A42, A62;

                  

                   A65: MX < (F . (m + 1)) by A42, A62;

                  now

                    assume (F . (m + 1)) <> M1;

                    then (F . (m + 1)) < M1 by A63, XXREAL_0: 1;

                    hence contradiction by A58, A65, A64;

                  end;

                  hence contradiction by A53;

                end;

                defpred X[ Nat] means (s . $1) > x0;

                 A66:

                now

                  let k;

                  consider n such that

                   A67: k <= n and

                   A68: (s . n) >= x0 by A23;

                  take n;

                  thus k <= n by A67;

                  (s . n) in ( rng s) by VALUED_0: 28;

                  then not (s . n) in {x0} by A16, XBOOLE_0:def 5;

                  then (s . n) <> x0 by TARSKI:def 1;

                  hence (s . n) > x0 by A68, XXREAL_0: 1;

                end;

                then ex mn be Element of NAT st 0 <= mn & (s . mn) > x0;

                then

                 A69: ex m be Nat st X[m];

                consider N be Nat such that

                 A70: X[N] & for n be Nat st X[n] holds N <= n from NAT_1:sch 5( A69);

                defpred X[ Nat] means ((s * F) . $1) < x0;

                

                 A71: for k be Nat st X[k] holds X[(k + 1)]

                proof

                  let k be Nat such that ((s * F) . k) < x0;

                   P[(F . k), (F . (k + 1))] by A42;

                  then (s . (F . (k + 1))) < x0;

                  hence thesis by FUNCT_2: 15;

                end;

                

                 A72: X[ 0 ] by A35, A42, FUNCT_2: 15;

                

                 A73: for k be Nat holds X[k] from NAT_1:sch 2( A72, A71);

                

                 A74: ( rng (s * F)) c= (( dom f) /\ ( left_open_halfline x0))

                proof

                  let x be object;

                  assume

                   A75: x in ( rng (s * F));

                  then

                  consider n such that

                   A76: ((s * F) . n) = x by FUNCT_2: 113;

                  ((s * F) . n) < x0 by A73;

                  then x in { g1 : g1 < x0 } by A76;

                  then

                   A77: x in ( left_open_halfline x0) by XXREAL_1: 229;

                  x in ( dom f) by A50, A75, XBOOLE_0:def 5;

                  hence thesis by A77, XBOOLE_0:def 4;

                end;

                defpred P[ set, set] means for n, m st $1 = n & $2 = m holds n < m & (s . m) > x0 & for k st n < k & (s . k) > x0 holds m <= k;

                defpred X[ Nat, set, set] means P[$2, $3];

                

                 A78: (s * F) is convergent by A14, A49, SEQ_4: 16;

                ( lim (s * F)) = x0 by A14, A15, A49, SEQ_4: 17;

                then

                 A79: (f /* (s * F)) is divergent_to-infty by A11, A78, A74, LIMFUNC2:def 3;

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

                 A80:

                now

                  let n;

                  consider m such that

                   A81: (n + 1) <= m and

                   A82: (s . m) > x0 by A66;

                  take m;

                  thus n < m & (s . m) > x0 by A81, A82, NAT_1: 13;

                end;

                

                 A83: for n be Nat holds for x be Element of NAT holds ex y be Element of NAT st X[n, x, y]

                proof

                  let n be Nat;

                  let x be Element of NAT ;

                  defpred X[ Nat] means x < $1 & (s . $1) > x0;

                  ex m st X[m] by A80;

                  then

                   A84: ex m be Nat st X[m];

                  consider l be Nat such that

                   A85: X[l] & for k be Nat st X[k] holds l <= k from NAT_1:sch 5( A84);

                  take l;

                  l in NAT by ORDINAL1:def 12;

                  hence thesis by A85;

                end;

                consider G be sequence of NAT such that

                 A86: (G . 0 ) = N9 & for n be Nat holds X[n, (G . n), (G . (n + 1))] from RECDEF_1:sch 2( A83);

                

                 A87: ( rng G) c= NAT by RELAT_1:def 19;

                then

                 A88: ( rng G) c= REAL by NUMBERS: 19;

                

                 A89: ( dom G) = NAT by FUNCT_2:def 1;

                then

                reconsider G as Real_Sequence by A88, RELSET_1: 4;

                 A90:

                now

                  let n;

                  (G . n) in ( rng G) by A89, FUNCT_1:def 3;

                  hence (G . n) is Element of NAT by A87;

                end;

                now

                  let n be Nat;

                  

                   A91: n in NAT by ORDINAL1:def 12;

                  

                   A92: (G . (n + 1)) is Element of NAT by A90;

                  (G . n) is Element of NAT by A90, A91;

                  hence (G . n) < (G . (n + 1)) by A86, A92;

                end;

                then

                reconsider G as increasing sequence of NAT by SEQM_3:def 6;

                

                 A93: (s * G) is subsequence of s by VALUED_0:def 17;

                then ( rng (s * G)) c= ( rng s) by VALUED_0: 21;

                then

                 A94: ( rng (s * G)) c= (( dom f) \ {x0}) by A16;

                defpred X[ Nat] means (s . $1) > x0 & for m holds (G . m) <> $1;

                

                 A95: for n st (s . n) > x0 holds ex m st (G . m) = n

                proof

                  assume ex n st X[n];

                  then

                   A96: ex n be Nat st X[n];

                  consider N1 be Nat such that

                   A97: X[N1] & for n be Nat st X[n] holds N1 <= n from NAT_1:sch 5( A96);

                  defpred X[ Nat] means $1 < N1 & (s . $1) > x0 & ex m st (G . m) = $1;

                  

                   A98: ex n be Nat st X[n]

                  proof

                    take N;

                    

                     A99: N <> N1 by A86, A97;

                    N <= N1 by A70, A97;

                    hence N < N1 by A99, XXREAL_0: 1;

                    thus (s . N) > x0 by A70;

                    take 0 ;

                    thus thesis by A86;

                  end;

                  

                   A100: for n be Nat st X[n] holds n <= N1;

                  consider NX be Nat such that

                   A101: X[NX] & for n be Nat st X[n] holds n <= NX from NAT_1:sch 6( A100, A98);

                  

                   A102: for k st NX < k & k < N1 holds (s . k) <= x0

                  proof

                    given k such that

                     A103: NX < k and

                     A104: k < N1 and

                     A105: (s . k) > x0;

                    now

                      per cases ;

                        suppose ex m st (G . m) = k;

                        hence contradiction by A101, A103, A104, A105;

                      end;

                        suppose for m holds (G . m) <> k;

                        hence contradiction by A97, A104, A105;

                      end;

                    end;

                    hence contradiction;

                  end;

                  consider m such that

                   A106: (G . m) = NX by A101;

                  N1 in NAT by ORDINAL1:def 12;

                  then

                   A107: (G . (m + 1)) <= N1 by A86, A97, A101, A106;

                  

                   A108: (s . (G . (m + 1))) > x0 by A86, A106;

                  

                   A109: NX < (G . (m + 1)) by A86, A106;

                  now

                    assume (G . (m + 1)) <> N1;

                    then (G . (m + 1)) < N1 by A107, XXREAL_0: 1;

                    hence contradiction by A102, A109, A108;

                  end;

                  hence contradiction by A97;

                end;

                defpred X[ Nat] means ((s * G) . $1) > x0;

                

                 A110: for k be Nat st X[k] holds X[(k + 1)]

                proof

                  let k be Nat such that ((s * G) . k) > x0;

                   P[(G . k), (G . (k + 1))] by A86;

                  then (s . (G . (k + 1))) > x0;

                  hence thesis by FUNCT_2: 15;

                end;

                

                 A111: X[ 0 ] by A70, A86, FUNCT_2: 15;

                

                 A112: for k be Nat holds X[k] from NAT_1:sch 2( A111, A110);

                

                 A113: ( rng (s * G)) c= (( dom f) /\ ( right_open_halfline x0))

                proof

                  let x be object;

                  assume

                   A114: x in ( rng (s * G));

                  then

                  consider n such that

                   A115: ((s * G) . n) = x by FUNCT_2: 113;

                  ((s * G) . n) > x0 by A112;

                  then x in { g1 : x0 < g1 } by A115;

                  then

                   A116: x in ( right_open_halfline x0) by XXREAL_1: 230;

                  x in ( dom f) by A94, A114, XBOOLE_0:def 5;

                  hence thesis by A116, XBOOLE_0:def 4;

                end;

                

                 A117: (s * G) is convergent by A14, A93, SEQ_4: 16;

                ( lim (s * G)) = x0 by A14, A15, A93, SEQ_4: 17;

                then

                 A118: (f /* (s * G)) is divergent_to-infty by A12, A117, A113, LIMFUNC2:def 6;

                now

                  let r;

                  consider n1 be Nat such that

                   A119: for k be Nat st n1 <= k holds ((f /* (s * F)) . k) < r by A79;

                  consider n2 be Nat such that

                   A120: for k be Nat st n2 <= k holds ((f /* (s * G)) . k) < r by A118;

                  reconsider n = ( max ((F . n1),(G . n2))) as Nat;

                  take n;

                  let k be Nat;

                  

                   A121: k in NAT by ORDINAL1:def 12;

                  assume

                   A122: n <= k;

                  (s . k) in ( rng s) by VALUED_0: 28;

                  then not (s . k) in {x0} by A16, XBOOLE_0:def 5;

                  then

                   A123: (s . k) <> x0 by TARSKI:def 1;

                  now

                    per cases by A123, XXREAL_0: 1;

                      suppose (s . k) < x0;

                      then

                      consider l be Element of NAT such that

                       A124: k = (F . l) by A51, A121;

                      (F . n1) <= n by XXREAL_0: 25;

                      then (F . n1) <= k by A122, XXREAL_0: 2;

                      then l >= n1 by A124, SEQM_3: 1;

                      then ((f /* (s * F)) . l) < r by A119;

                      then (f . ((s * F) . l)) < r by A50, FUNCT_2: 108, XBOOLE_1: 1;

                      then (f . (s . k)) < r by A124, FUNCT_2: 15;

                      hence ((f /* s) . k) < r by A16, FUNCT_2: 108, XBOOLE_1: 1, A121;

                    end;

                      suppose (s . k) > x0;

                      then

                      consider l be Element of NAT such that

                       A125: k = (G . l) by A95, A121;

                      (G . n2) <= n by XXREAL_0: 25;

                      then (G . n2) <= k by A122, XXREAL_0: 2;

                      then l >= n2 by A125, SEQM_3: 1;

                      then ((f /* (s * G)) . l) < r by A120;

                      then (f . ((s * G) . l)) < r by A94, FUNCT_2: 108, XBOOLE_1: 1;

                      then (f . (s . k)) < r by A125, FUNCT_2: 15;

                      hence ((f /* s) . k) < r by A16, FUNCT_2: 108, XBOOLE_1: 1, A121;

                    end;

                  end;

                  hence ((f /* s) . k) < r;

                end;

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

              end;

            end;

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

          end;

        end;

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

      end;

      now

        let r1, r2;

        assume that

         A126: r1 < x0 and

         A127: x0 < r2;

        consider g1 such that

         A128: r1 < g1 and

         A129: g1 < x0 and

         A130: g1 in ( dom f) by A11, A126, LIMFUNC2:def 3;

        consider g2 such that

         A131: g2 < r2 and

         A132: x0 < g2 and

         A133: g2 in ( dom f) by A12, A127, LIMFUNC2:def 6;

        take g1;

        take g2;

        thus r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) by A128, A129, A130, A131, A132, A133;

      end;

      hence thesis by A13;

    end;

    theorem :: LIMFUNC3:14

    f1 is_divergent_to+infty_in x0 & f2 is_divergent_to+infty_in x0 & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in (( dom f1) /\ ( dom f2)) & g2 < r2 & x0 < g2 & g2 in (( dom f1) /\ ( dom f2))) implies (f1 + f2) is_divergent_to+infty_in x0 & (f1 (#) f2) is_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_divergent_to+infty_in x0 and

       A2: f2 is_divergent_to+infty_in x0 and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in (( dom f1) /\ ( dom f2)) & g2 < r2 & x0 < g2 & g2 in (( dom f1) /\ ( dom f2));

       A4:

      now

        let s be Real_Sequence;

        assume that

         A5: s is convergent and

         A6: ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f1 + f2)) \ {x0});

        ( rng s) c= (( dom f2) \ {x0}) by A7, Lm4;

        then

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

        ( rng s) c= (( dom f1) \ {x0}) by A7, Lm4;

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

        then

         A9: ((f1 /* s) + (f2 /* s)) is divergent_to+infty by A8, LIMFUNC1: 8;

        

         A10: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by A7, Lm4;

        ( rng s) c= ( dom (f1 + f2)) by A7, Lm4;

        hence ((f1 + f2) /* s) is divergent_to+infty by A10, A9, RFUNCT_2: 8;

      end;

       A11:

      now

        let s be Real_Sequence;

        assume that

         A12: s is convergent and

         A13: ( lim s) = x0 and

         A14: ( rng s) c= (( dom (f1 (#) f2)) \ {x0});

        ( rng s) c= (( dom f2) \ {x0}) by A14, Lm2;

        then

         A15: (f2 /* s) is divergent_to+infty by A2, A12, A13;

        ( rng s) c= (( dom f1) \ {x0}) by A14, Lm2;

        then (f1 /* s) is divergent_to+infty by A1, A12, A13;

        then

         A16: ((f1 /* s) (#) (f2 /* s)) is divergent_to+infty by A15, LIMFUNC1: 10;

        

         A17: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by A14, Lm2;

        ( rng s) c= ( dom (f1 (#) f2)) by A14, Lm2;

        hence ((f1 (#) f2) /* s) is divergent_to+infty by A17, A16, RFUNCT_2: 8;

      end;

      now

        let r1, r2;

        assume that

         A18: r1 < x0 and

         A19: x0 < r2;

        consider g1, g2 such that

         A20: r1 < g1 and

         A21: g1 < x0 and

         A22: g1 in (( dom f1) /\ ( dom f2)) and

         A23: g2 < r2 and

         A24: x0 < g2 and

         A25: g2 in (( dom f1) /\ ( dom f2)) by A3, A18, A19;

        take g1;

        take g2;

        thus r1 < g1 & g1 < x0 & g1 in ( dom (f1 + f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 + f2)) by A20, A21, A22, A23, A24, A25, VALUED_1:def 1;

      end;

      hence (f1 + f2) is_divergent_to+infty_in x0 by A4;

      now

        let r1, r2;

        assume that

         A26: r1 < x0 and

         A27: x0 < r2;

        consider g1, g2 such that

         A28: r1 < g1 and

         A29: g1 < x0 and

         A30: g1 in (( dom f1) /\ ( dom f2)) and

         A31: g2 < r2 and

         A32: x0 < g2 and

         A33: g2 in (( dom f1) /\ ( dom f2)) by A3, A26, A27;

        take g1;

        take g2;

        thus r1 < g1 & g1 < x0 & g1 in ( dom (f1 (#) f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 (#) f2)) by A28, A29, A30, A31, A32, A33, VALUED_1:def 4;

      end;

      hence thesis by A11;

    end;

    theorem :: LIMFUNC3:15

    f1 is_divergent_to-infty_in x0 & f2 is_divergent_to-infty_in x0 & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in (( dom f1) /\ ( dom f2)) & g2 < r2 & x0 < g2 & g2 in (( dom f1) /\ ( dom f2))) implies (f1 + f2) is_divergent_to-infty_in x0 & (f1 (#) f2) is_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_divergent_to-infty_in x0 and

       A2: f2 is_divergent_to-infty_in x0 and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in (( dom f1) /\ ( dom f2)) & g2 < r2 & x0 < g2 & g2 in (( dom f1) /\ ( dom f2));

       A4:

      now

        let s be Real_Sequence;

        assume that

         A5: s is convergent and

         A6: ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f1 + f2)) \ {x0});

        ( rng s) c= (( dom f2) \ {x0}) by A7, Lm4;

        then

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

        ( rng s) c= (( dom f1) \ {x0}) by A7, Lm4;

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

        then

         A9: ((f1 /* s) + (f2 /* s)) is divergent_to-infty by A8, LIMFUNC1: 11;

        

         A10: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by A7, Lm4;

        ( rng s) c= ( dom (f1 + f2)) by A7, Lm4;

        hence ((f1 + f2) /* s) is divergent_to-infty by A10, A9, RFUNCT_2: 8;

      end;

       A11:

      now

        let s be Real_Sequence;

        assume that

         A12: s is convergent and

         A13: ( lim s) = x0 and

         A14: ( rng s) c= (( dom (f1 (#) f2)) \ {x0});

        ( rng s) c= (( dom f2) \ {x0}) by A14, Lm2;

        then

         A15: (f2 /* s) is divergent_to-infty by A2, A12, A13;

        ( rng s) c= (( dom f1) \ {x0}) by A14, Lm2;

        then (f1 /* s) is divergent_to-infty by A1, A12, A13;

        then

         A16: ((f1 /* s) (#) (f2 /* s)) is divergent_to+infty by A15, LIMFUNC1: 24;

        

         A17: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by A14, Lm2;

        ( rng s) c= ( dom (f1 (#) f2)) by A14, Lm2;

        hence ((f1 (#) f2) /* s) is divergent_to+infty by A17, A16, RFUNCT_2: 8;

      end;

      now

        let r1, r2;

        assume that

         A18: r1 < x0 and

         A19: x0 < r2;

        consider g1, g2 such that

         A20: r1 < g1 and

         A21: g1 < x0 and

         A22: g1 in (( dom f1) /\ ( dom f2)) and

         A23: g2 < r2 and

         A24: x0 < g2 and

         A25: g2 in (( dom f1) /\ ( dom f2)) by A3, A18, A19;

        take g1;

        take g2;

        thus r1 < g1 & g1 < x0 & g1 in ( dom (f1 + f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 + f2)) by A20, A21, A22, A23, A24, A25, VALUED_1:def 1;

      end;

      hence (f1 + f2) is_divergent_to-infty_in x0 by A4;

      now

        let r1, r2;

        assume that

         A26: r1 < x0 and

         A27: x0 < r2;

        consider g1, g2 such that

         A28: r1 < g1 and

         A29: g1 < x0 and

         A30: g1 in (( dom f1) /\ ( dom f2)) and

         A31: g2 < r2 and

         A32: x0 < g2 and

         A33: g2 in (( dom f1) /\ ( dom f2)) by A3, A26, A27;

        take g1;

        take g2;

        thus r1 < g1 & g1 < x0 & g1 in ( dom (f1 (#) f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 (#) f2)) by A28, A29, A30, A31, A32, A33, VALUED_1:def 4;

      end;

      hence thesis by A11;

    end;

    theorem :: LIMFUNC3:16

    f1 is_divergent_to+infty_in x0 & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f1 + f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 + f2))) & (ex r st 0 < r & (f2 | ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) is bounded_below) implies (f1 + f2) is_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_divergent_to+infty_in x0 and

       A2: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f1 + f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 + f2));

      given r such that

       A3: 0 < r and

       A4: (f2 | ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) is bounded_below;

      now

        let s be Real_Sequence;

        assume that

         A5: s is convergent and

         A6: ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f1 + f2)) \ {x0});

        consider k such that

         A8: for n st k <= n holds (x0 - r) < (s . n) & (s . n) < (x0 + r) by A3, A5, A6, Th7;

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

        then

         A9: ( rng (s ^\ k)) c= (( dom (f1 + f2)) \ {x0}) by A7;

        then

         A10: ( rng (s ^\ k)) c= (( dom f1) \ {x0}) by Lm4;

        

         A11: ( rng (s ^\ k)) c= ( dom f2) by A9, Lm4;

        now

          consider r1 be Real such that

           A12: for g be object st g in (( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) /\ ( dom f2)) holds r1 <= (f2 . g) by A4, RFUNCT_1: 71;

          take r2 = (r1 - 1);

          let n be Nat;

          

           A13: n in NAT by ORDINAL1:def 12;

          

           A14: k <= (n + k) by NAT_1: 12;

          then (s . (n + k)) < (x0 + r) by A8;

          then

           A15: ((s ^\ k) . n) < (x0 + r) by NAT_1:def 3;

          (x0 - r) < (s . (n + k)) by A8, A14;

          then (x0 - r) < ((s ^\ k) . n) by NAT_1:def 3;

          then ((s ^\ k) . n) in { g2 : (x0 - r) < g2 & g2 < (x0 + r) } by A15;

          then

           A16: ((s ^\ k) . n) in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

          

           A17: ((s ^\ k) . n) in ( rng (s ^\ k)) by VALUED_0: 28;

          then not ((s ^\ k) . n) in {x0} by A9, XBOOLE_0:def 5;

          then ((s ^\ k) . n) in ( ].(x0 - r), (x0 + r).[ \ {x0}) by A16, XBOOLE_0:def 5;

          then ((s ^\ k) . n) in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by A3, Th4;

          then ((s ^\ k) . n) in (( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) /\ ( dom f2)) by A11, A17, XBOOLE_0:def 4;

          then (r1 - 1) < ((f2 . ((s ^\ k) . n)) - 0 ) by A12, XREAL_1: 15;

          hence r2 < ((f2 /* (s ^\ k)) . n) by A11, FUNCT_2: 108, A13;

        end;

        then

         A18: (f2 /* (s ^\ k)) is bounded_below by SEQ_2:def 4;

        ( lim (s ^\ k)) = x0 by A5, A6, SEQ_4: 20;

        then (f1 /* (s ^\ k)) is divergent_to+infty by A1, A5, A10;

        then

         A19: ((f1 /* (s ^\ k)) + (f2 /* (s ^\ k))) is divergent_to+infty by A18, LIMFUNC1: 9;

        

         A20: ( rng s) c= ( dom (f1 + f2)) by A7, Lm4;

        ( rng (s ^\ k)) c= ( dom (f1 + f2)) by A9, Lm4;

        then ( rng (s ^\ k)) c= (( dom f1) /\ ( dom f2)) by VALUED_1:def 1;

        

        then ((f1 /* (s ^\ k)) + (f2 /* (s ^\ k))) = ((f1 + f2) /* (s ^\ k)) by RFUNCT_2: 8

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

        hence ((f1 + f2) /* s) is divergent_to+infty by A19, LIMFUNC1: 7;

      end;

      hence thesis by A2;

    end;

    theorem :: LIMFUNC3:17

    f1 is_divergent_to+infty_in x0 & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f1 (#) f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 (#) f2))) & (ex r, r1 st 0 < r & 0 < r1 & for g st g in (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds r1 <= (f2 . g)) implies (f1 (#) f2) is_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_divergent_to+infty_in x0 and

       A2: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f1 (#) f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 (#) f2));

      given r, t such that

       A3: 0 < r and

       A4: 0 < t and

       A5: for g st g in (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds t <= (f2 . g);

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent and

         A7: ( lim s) = x0 and

         A8: ( rng s) c= (( dom (f1 (#) f2)) \ {x0});

        consider k such that

         A9: for n st k <= n holds (x0 - r) < (s . n) & (s . n) < (x0 + r) by A3, A6, A7, Th7;

        

         A10: ( rng s) c= ( dom (f1 (#) f2)) by A8, Lm2;

        

         A11: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by A8, Lm2;

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

        then

         A12: ( rng (s ^\ k)) c= (( dom (f1 (#) f2)) \ {x0}) by A8;

        then

         A13: ( rng (s ^\ k)) c= (( dom f1) \ {x0}) by Lm2;

        

         A14: ( rng (s ^\ k)) c= ( dom f2) by A12, Lm2;

         A15:

        now

          thus 0 < t by A4;

          let n be Nat;

          

           A16: n in NAT by ORDINAL1:def 12;

          

           A17: k <= (n + k) by NAT_1: 12;

          then (s . (n + k)) < (x0 + r) by A9;

          then

           A18: ((s ^\ k) . n) < (x0 + r) by NAT_1:def 3;

          (x0 - r) < (s . (n + k)) by A9, A17;

          then (x0 - r) < ((s ^\ k) . n) by NAT_1:def 3;

          then ((s ^\ k) . n) in { g2 : (x0 - r) < g2 & g2 < (x0 + r) } by A18;

          then

           A19: ((s ^\ k) . n) in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

          

           A20: ((s ^\ k) . n) in ( rng (s ^\ k)) by VALUED_0: 28;

          then not ((s ^\ k) . n) in {x0} by A12, XBOOLE_0:def 5;

          then ((s ^\ k) . n) in ( ].(x0 - r), (x0 + r).[ \ {x0}) by A19, XBOOLE_0:def 5;

          then ((s ^\ k) . n) in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by A3, Th4;

          then ((s ^\ k) . n) in (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A14, A20, XBOOLE_0:def 4;

          then t <= (f2 . ((s ^\ k) . n)) by A5;

          hence t <= ((f2 /* (s ^\ k)) . n) by A14, FUNCT_2: 108, A16;

        end;

        ( lim (s ^\ k)) = x0 by A6, A7, SEQ_4: 20;

        then (f1 /* (s ^\ k)) is divergent_to+infty by A1, A6, A13;

        then

         A21: ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) is divergent_to+infty by A15, LIMFUNC1: 22;

        ( rng (s ^\ k)) c= ( dom (f1 (#) f2)) by A12, Lm2;

        

        then ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) = ((f1 (#) f2) /* (s ^\ k)) by A11, RFUNCT_2: 8

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

        hence ((f1 (#) f2) /* s) is divergent_to+infty by A21, LIMFUNC1: 7;

      end;

      hence thesis by A2;

    end;

    theorem :: LIMFUNC3:18

    (f is_divergent_to+infty_in x0 & r > 0 implies (r (#) f) is_divergent_to+infty_in x0) & (f is_divergent_to+infty_in x0 & r < 0 implies (r (#) f) is_divergent_to-infty_in x0) & (f is_divergent_to-infty_in x0 & r > 0 implies (r (#) f) is_divergent_to-infty_in x0) & (f is_divergent_to-infty_in x0 & r < 0 implies (r (#) f) is_divergent_to+infty_in x0)

    proof

      thus f is_divergent_to+infty_in x0 & r > 0 implies (r (#) f) is_divergent_to+infty_in x0

      proof

        assume that

         A1: f is_divergent_to+infty_in x0 and

         A2: r > 0 ;

        thus for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (r (#) f)) & g2 < r2 & x0 < g2 & g2 in ( dom (r (#) f))

        proof

          let r1, r2;

          assume that

           A3: r1 < x0 and

           A4: x0 < r2;

          consider g1, g2 such that

           A5: r1 < g1 and

           A6: g1 < x0 and

           A7: g1 in ( dom f) and

           A8: g2 < r2 and

           A9: x0 < g2 and

           A10: g2 in ( dom f) by A1, A3, A4;

          take g1;

          take g2;

          thus thesis by A5, A6, A7, A8, A9, A10, VALUED_1:def 5;

        end;

        let seq;

        assume that

         A11: seq is convergent and

         A12: ( lim seq) = x0 and

         A13: ( rng seq) c= (( dom (r (#) f)) \ {x0});

        

         A14: ( rng seq) c= (( dom f) \ {x0}) by A13, VALUED_1:def 5;

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

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

        hence thesis by A14, RFUNCT_2: 9, XBOOLE_1: 1;

      end;

      thus f is_divergent_to+infty_in x0 & r < 0 implies (r (#) f) is_divergent_to-infty_in x0

      proof

        assume that

         A15: f is_divergent_to+infty_in x0 and

         A16: r < 0 ;

        thus for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (r (#) f)) & g2 < r2 & x0 < g2 & g2 in ( dom (r (#) f))

        proof

          let r1, r2;

          assume that

           A17: r1 < x0 and

           A18: x0 < r2;

          consider g1, g2 such that

           A19: r1 < g1 and

           A20: g1 < x0 and

           A21: g1 in ( dom f) and

           A22: g2 < r2 and

           A23: x0 < g2 and

           A24: g2 in ( dom f) by A15, A17, A18;

          take g1;

          take g2;

          thus thesis by A19, A20, A21, A22, A23, A24, VALUED_1:def 5;

        end;

        let seq;

        assume that

         A25: seq is convergent and

         A26: ( lim seq) = x0 and

         A27: ( rng seq) c= (( dom (r (#) f)) \ {x0});

        

         A28: ( rng seq) c= (( dom f) \ {x0}) by A27, VALUED_1:def 5;

        then (f /* seq) is divergent_to+infty by A15, A25, A26;

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

        hence thesis by A28, RFUNCT_2: 9, XBOOLE_1: 1;

      end;

      thus f is_divergent_to-infty_in x0 & r > 0 implies (r (#) f) is_divergent_to-infty_in x0

      proof

        assume that

         A29: f is_divergent_to-infty_in x0 and

         A30: r > 0 ;

        thus for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (r (#) f)) & g2 < r2 & x0 < g2 & g2 in ( dom (r (#) f))

        proof

          let r1, r2;

          assume that

           A31: r1 < x0 and

           A32: x0 < r2;

          consider g1, g2 such that

           A33: r1 < g1 and

           A34: g1 < x0 and

           A35: g1 in ( dom f) and

           A36: g2 < r2 and

           A37: x0 < g2 and

           A38: g2 in ( dom f) by A29, A31, A32;

          take g1;

          take g2;

          thus thesis by A33, A34, A35, A36, A37, A38, VALUED_1:def 5;

        end;

        let seq;

        assume that

         A39: seq is convergent and

         A40: ( lim seq) = x0 and

         A41: ( rng seq) c= (( dom (r (#) f)) \ {x0});

        

         A42: ( rng seq) c= (( dom f) \ {x0}) by A41, VALUED_1:def 5;

        then (f /* seq) is divergent_to-infty by A29, A39, A40;

        then (r (#) (f /* seq)) is divergent_to-infty by A30, LIMFUNC1: 14;

        hence thesis by A42, RFUNCT_2: 9, XBOOLE_1: 1;

      end;

      assume that

       A43: f is_divergent_to-infty_in x0 and

       A44: r < 0 ;

      thus for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (r (#) f)) & g2 < r2 & x0 < g2 & g2 in ( dom (r (#) f))

      proof

        let r1, r2;

        assume that

         A45: r1 < x0 and

         A46: x0 < r2;

        consider g1, g2 such that

         A47: r1 < g1 and

         A48: g1 < x0 and

         A49: g1 in ( dom f) and

         A50: g2 < r2 and

         A51: x0 < g2 and

         A52: g2 in ( dom f) by A43, A45, A46;

        take g1;

        take g2;

        thus thesis by A47, A48, A49, A50, A51, A52, VALUED_1:def 5;

      end;

      let seq;

      assume that

       A53: seq is convergent and

       A54: ( lim seq) = x0 and

       A55: ( rng seq) c= (( dom (r (#) f)) \ {x0});

      

       A56: ( rng seq) c= (( dom f) \ {x0}) by A55, VALUED_1:def 5;

      then (f /* seq) is divergent_to-infty by A43, A53, A54;

      then (r (#) (f /* seq)) is divergent_to+infty by A44, LIMFUNC1: 14;

      hence thesis by A56, RFUNCT_2: 9, XBOOLE_1: 1;

    end;

    theorem :: LIMFUNC3:19

    (f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0) implies ( abs f) is_divergent_to+infty_in x0

    proof

      assume

       A1: f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0;

      now

        per cases by A1;

          suppose

           A2: f is_divergent_to+infty_in x0;

           A3:

          now

            let seq;

            assume that

             A4: seq is convergent and

             A5: ( lim seq) = x0 and

             A6: ( rng seq) c= (( dom ( abs f)) \ {x0});

            

             A7: ( rng seq) c= (( dom f) \ {x0}) by A6, VALUED_1:def 11;

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

            then

             A8: ( abs (f /* seq)) is divergent_to+infty by LIMFUNC1: 25;

            ( rng seq) c= ( dom f) by A7, XBOOLE_1: 1;

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

          end;

          now

            let r1, r2;

            assume that

             A9: r1 < x0 and

             A10: x0 < r2;

            consider g1, g2 such that

             A11: r1 < g1 and

             A12: g1 < x0 and

             A13: g1 in ( dom f) and

             A14: g2 < r2 and

             A15: x0 < g2 and

             A16: g2 in ( dom f) by A2, A9, A10;

            take g1;

            take g2;

            thus r1 < g1 & g1 < x0 & g1 in ( dom ( abs f)) & g2 < r2 & x0 < g2 & g2 in ( dom ( abs f)) by A11, A12, A13, A14, A15, A16, VALUED_1:def 11;

          end;

          hence thesis by A3;

        end;

          suppose

           A17: f is_divergent_to-infty_in x0;

           A18:

          now

            let seq;

            assume that

             A19: seq is convergent and

             A20: ( lim seq) = x0 and

             A21: ( rng seq) c= (( dom ( abs f)) \ {x0});

            

             A22: ( rng seq) c= (( dom f) \ {x0}) by A21, VALUED_1:def 11;

            then (f /* seq) is divergent_to-infty by A17, A19, A20;

            then

             A23: ( abs (f /* seq)) is divergent_to+infty by LIMFUNC1: 25;

            ( rng seq) c= ( dom f) by A22, XBOOLE_1: 1;

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

          end;

          now

            let r1, r2;

            assume that

             A24: r1 < x0 and

             A25: x0 < r2;

            consider g1, g2 such that

             A26: r1 < g1 and

             A27: g1 < x0 and

             A28: g1 in ( dom f) and

             A29: g2 < r2 and

             A30: x0 < g2 and

             A31: g2 in ( dom f) by A17, A24, A25;

            take g1;

            take g2;

            thus r1 < g1 & g1 < x0 & g1 in ( dom ( abs f)) & g2 < r2 & x0 < g2 & g2 in ( dom ( abs f)) by A26, A27, A28, A29, A30, A31, VALUED_1:def 11;

          end;

          hence thesis by A18;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC3:20

    

     Th20: (ex r st (f | ].(x0 - r), x0.[) is non-decreasing & (f | ].x0, (x0 + r).[) is non-increasing & not (f | ].(x0 - r), x0.[) is bounded_above & not (f | ].x0, (x0 + r).[) is bounded_above) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) implies f is_divergent_to+infty_in x0

    proof

      given r such that

       A1: (f | ].(x0 - r), x0.[) is non-decreasing and

       A2: (f | ].x0, (x0 + r).[) is non-increasing and

       A3: not (f | ].(x0 - r), x0.[) is bounded_above and

       A4: not (f | ].x0, (x0 + r).[) is bounded_above;

      assume

       A5: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f);

      then for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom f) by Th8;

      then

       A6: f is_right_divergent_to+infty_in x0 by A2, A4, LIMFUNC2: 29;

      for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom f) by A5, Th8;

      then f is_left_divergent_to+infty_in x0 by A1, A3, LIMFUNC2: 25;

      hence thesis by A6, Th12;

    end;

    theorem :: LIMFUNC3:21

    (ex r st 0 < r & (f | ].(x0 - r), x0.[) is increasing & (f | ].x0, (x0 + r).[) is decreasing & not (f | ].(x0 - r), x0.[) is bounded_above & not (f | ].x0, (x0 + r).[) is bounded_above) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) implies f is_divergent_to+infty_in x0 by Th20;

    theorem :: LIMFUNC3:22

    

     Th22: (ex r st (f | ].(x0 - r), x0.[) is non-increasing & (f | ].x0, (x0 + r).[) is non-decreasing & not (f | ].(x0 - r), x0.[) is bounded_below & not (f | ].x0, (x0 + r).[) is bounded_below) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) implies f is_divergent_to-infty_in x0

    proof

      given r such that

       A1: (f | ].(x0 - r), x0.[) is non-increasing and

       A2: (f | ].x0, (x0 + r).[) is non-decreasing and

       A3: not (f | ].(x0 - r), x0.[) is bounded_below and

       A4: not (f | ].x0, (x0 + r).[) is bounded_below;

      assume

       A5: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f);

      then for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom f) by Th8;

      then

       A6: f is_right_divergent_to-infty_in x0 by A2, A4, LIMFUNC2: 31;

      for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom f) by A5, Th8;

      then f is_left_divergent_to-infty_in x0 by A1, A3, LIMFUNC2: 27;

      hence thesis by A6, Th13;

    end;

    theorem :: LIMFUNC3:23

    (ex r st 0 < r & (f | ].(x0 - r), x0.[) is decreasing & (f | ].x0, (x0 + r).[) is increasing & not (f | ].(x0 - r), x0.[) is bounded_below & not (f | ].x0, (x0 + r).[) is bounded_below) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) implies f is_divergent_to-infty_in x0 by Th22;

    theorem :: LIMFUNC3:24

    

     Th24: f1 is_divergent_to+infty_in x0 & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) & (ex r st 0 < r & (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) c= (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) & for g st g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f1 . g) <= (f . g)) implies f is_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_divergent_to+infty_in x0 and

       A2: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f);

      given r such that

       A3: 0 < r and

       A4: (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) c= (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) and

       A5: for g st g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f1 . g) <= (f . g);

      thus for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) by A2;

      let s be Real_Sequence;

      assume that

       A6: s is convergent and

       A7: ( lim s) = x0 and

       A8: ( rng s) c= (( dom f) \ {x0});

      consider k such that

       A9: for n st k <= n holds (x0 - r) < (s . n) & (s . n) < (x0 + r) by A3, A6, A7, Th7;

      

       A10: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

      then

       A11: ( rng (s ^\ k)) c= (( dom f) \ {x0}) by A8;

      now

        let x be object;

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

        then

        consider n such that

         A12: ((s ^\ k) . n) = x by FUNCT_2: 113;

        

         A13: k <= (n + k) by NAT_1: 12;

        then (s . (n + k)) < (x0 + r) by A9;

        then

         A14: ((s ^\ k) . n) < (x0 + r) by NAT_1:def 3;

        (x0 - r) < (s . (n + k)) by A9, A13;

        then (x0 - r) < ((s ^\ k) . n) by NAT_1:def 3;

        then ((s ^\ k) . n) in { g1 : (x0 - r) < g1 & g1 < (x0 + r) } by A14;

        then

         A15: ((s ^\ k) . n) in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        ((s ^\ k) . n) in ( rng (s ^\ k)) by VALUED_0: 28;

        then not ((s ^\ k) . n) in {x0} by A11, XBOOLE_0:def 5;

        then ((s ^\ k) . n) in ( ].(x0 - r), (x0 + r).[ \ {x0}) by A15, XBOOLE_0:def 5;

        hence x in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by A3, A12, Th4;

      end;

      then

       A16: ( rng (s ^\ k)) c= ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[);

      

       A17: ( rng s) c= ( dom f) by A8, XBOOLE_1: 1;

      then ( rng (s ^\ k)) c= ( dom f) by A10;

      then

       A18: ( rng (s ^\ k)) c= (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A16, XBOOLE_1: 19;

      then

       A19: ( rng (s ^\ k)) c= (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A4;

       A20:

      now

        let n be Nat;

        

         A21: n in NAT by ORDINAL1:def 12;

        ((s ^\ k) . n) in ( rng (s ^\ k)) by VALUED_0: 28;

        then (f1 . ((s ^\ k) . n)) <= (f . ((s ^\ k) . n)) by A5, A18;

        then ((f1 /* (s ^\ k)) . n) <= (f . ((s ^\ k) . n)) by A19, FUNCT_2: 108, XBOOLE_1: 18, A21;

        hence ((f1 /* (s ^\ k)) . n) <= ((f /* (s ^\ k)) . n) by A17, A10, FUNCT_2: 108, XBOOLE_1: 1, A21;

      end;

      

       A22: ( rng (s ^\ k)) c= ( dom f1) by A19, XBOOLE_1: 18;

      now

        let x be object;

        assume

         A23: x in ( rng (s ^\ k));

        then not x in {x0} by A11, XBOOLE_0:def 5;

        hence x in (( dom f1) \ {x0}) by A22, A23, XBOOLE_0:def 5;

      end;

      then

       A24: ( rng (s ^\ k)) c= (( dom f1) \ {x0});

      ( lim (s ^\ k)) = x0 by A6, A7, SEQ_4: 20;

      then (f1 /* (s ^\ k)) is divergent_to+infty by A1, A6, A24;

      then (f /* (s ^\ k)) is divergent_to+infty by A20, LIMFUNC1: 42;

      then ((f /* s) ^\ k) is divergent_to+infty by A8, VALUED_0: 27, XBOOLE_1: 1;

      hence thesis by LIMFUNC1: 7;

    end;

    theorem :: LIMFUNC3:25

    

     Th25: f1 is_divergent_to-infty_in x0 & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) & (ex r st 0 < r & (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) c= (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) & for g st g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f . g) <= (f1 . g)) implies f is_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_divergent_to-infty_in x0 and

       A2: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f);

      given r such that

       A3: 0 < r and

       A4: (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) c= (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) and

       A5: for g st g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f . g) <= (f1 . g);

      thus for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) by A2;

      let s be Real_Sequence;

      assume that

       A6: s is convergent and

       A7: ( lim s) = x0 and

       A8: ( rng s) c= (( dom f) \ {x0});

      consider k such that

       A9: for n st k <= n holds (x0 - r) < (s . n) & (s . n) < (x0 + r) by A3, A6, A7, Th7;

      

       A10: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

      then

       A11: ( rng (s ^\ k)) c= (( dom f) \ {x0}) by A8;

      now

        let x be object;

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

        then

        consider n such that

         A12: ((s ^\ k) . n) = x by FUNCT_2: 113;

        

         A13: k <= (n + k) by NAT_1: 12;

        then (s . (n + k)) < (x0 + r) by A9;

        then

         A14: ((s ^\ k) . n) < (x0 + r) by NAT_1:def 3;

        (x0 - r) < (s . (n + k)) by A9, A13;

        then (x0 - r) < ((s ^\ k) . n) by NAT_1:def 3;

        then ((s ^\ k) . n) in { g1 : (x0 - r) < g1 & g1 < (x0 + r) } by A14;

        then

         A15: ((s ^\ k) . n) in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        ((s ^\ k) . n) in ( rng (s ^\ k)) by VALUED_0: 28;

        then not ((s ^\ k) . n) in {x0} by A11, XBOOLE_0:def 5;

        then ((s ^\ k) . n) in ( ].(x0 - r), (x0 + r).[ \ {x0}) by A15, XBOOLE_0:def 5;

        hence x in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by A3, A12, Th4;

      end;

      then

       A16: ( rng (s ^\ k)) c= ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[);

      

       A17: ( rng s) c= ( dom f) by A8, XBOOLE_1: 1;

      then ( rng (s ^\ k)) c= ( dom f) by A10;

      then

       A18: ( rng (s ^\ k)) c= (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A16, XBOOLE_1: 19;

      then

       A19: ( rng (s ^\ k)) c= (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A4;

       A20:

      now

        let n be Nat;

        

         A21: n in NAT by ORDINAL1:def 12;

        ((s ^\ k) . n) in ( rng (s ^\ k)) by VALUED_0: 28;

        then (f . ((s ^\ k) . n)) <= (f1 . ((s ^\ k) . n)) by A5, A18;

        then ((f /* (s ^\ k)) . n) <= (f1 . ((s ^\ k) . n)) by A17, A10, FUNCT_2: 108, XBOOLE_1: 1, A21;

        hence ((f /* (s ^\ k)) . n) <= ((f1 /* (s ^\ k)) . n) by A19, FUNCT_2: 108, XBOOLE_1: 18, A21;

      end;

      

       A22: ( rng (s ^\ k)) c= ( dom f1) by A19, XBOOLE_1: 18;

      now

        let x be object;

        assume

         A23: x in ( rng (s ^\ k));

        then not x in {x0} by A11, XBOOLE_0:def 5;

        hence x in (( dom f1) \ {x0}) by A22, A23, XBOOLE_0:def 5;

      end;

      then

       A24: ( rng (s ^\ k)) c= (( dom f1) \ {x0});

      ( lim (s ^\ k)) = x0 by A6, A7, SEQ_4: 20;

      then (f1 /* (s ^\ k)) is divergent_to-infty by A1, A6, A24;

      then (f /* (s ^\ k)) is divergent_to-infty by A20, LIMFUNC1: 43;

      then ((f /* s) ^\ k) is divergent_to-infty by A8, VALUED_0: 27, XBOOLE_1: 1;

      hence thesis by LIMFUNC1: 7;

    end;

    theorem :: LIMFUNC3:26

    f1 is_divergent_to+infty_in x0 & (ex r st 0 < r & ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) c= (( dom f) /\ ( dom f1)) & for g st g in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) holds (f1 . g) <= (f . g)) implies f is_divergent_to+infty_in x0

    proof

      assume

       A1: f1 is_divergent_to+infty_in x0;

      given r such that

       A2: 0 < r and

       A3: ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) c= (( dom f) /\ ( dom f1)) and

       A4: for g st g in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) holds (f1 . g) <= (f . g);

      

       A5: ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) = (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A3, XBOOLE_1: 18, XBOOLE_1: 28;

      

       A6: ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) = (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A3, XBOOLE_1: 18, XBOOLE_1: 28;

      for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) by A2, A3, Th5, XBOOLE_1: 18;

      hence thesis by A1, A2, A4, A5, A6, Th24;

    end;

    theorem :: LIMFUNC3:27

    f1 is_divergent_to-infty_in x0 & (ex r st 0 < r & ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) c= (( dom f) /\ ( dom f1)) & for g st g in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) holds (f . g) <= (f1 . g)) implies f is_divergent_to-infty_in x0

    proof

      assume

       A1: f1 is_divergent_to-infty_in x0;

      given r such that

       A2: 0 < r and

       A3: ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) c= (( dom f) /\ ( dom f1)) and

       A4: for g st g in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) holds (f . g) <= (f1 . g);

      

       A5: ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) = (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A3, XBOOLE_1: 18, XBOOLE_1: 28;

      

       A6: ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) = (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A3, XBOOLE_1: 18, XBOOLE_1: 28;

      for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) by A2, A3, Th5, XBOOLE_1: 18;

      hence thesis by A1, A2, A4, A5, A6, Th25;

    end;

    definition

      let f, x0;

      assume

       A1: f is_convergent_in x0;

      :: LIMFUNC3:def4

      func lim (f,x0) -> Real means

      : Def4: for seq st seq is convergent & ( lim seq) = x0 & ( rng seq) c= (( dom f) \ {x0}) holds (f /* seq) is convergent & ( lim (f /* seq)) = it ;

      existence by A1;

      uniqueness

      proof

        defpred X[ Element of NAT , Real] means (x0 - (1 / ($1 + 1))) < $2 & $2 < x0 & $2 in ( dom f);

         A2:

        now

          let n;

          

           A3: (x0 + 0 ) < (x0 + 1) by XREAL_1: 8;

          (x0 - (1 / (n + 1))) < x0 by Lm3;

          then

          consider g1, g2 such that

           A4: (x0 - (1 / (n + 1))) < g1 and

           A5: g1 < x0 and

           A6: g1 in ( dom f) and g2 < (x0 + 1) and x0 < g2 and g2 in ( dom f) by A1, A3;

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

          take g1;

          thus X[n, g1] by A4, A5, A6;

        end;

        consider s be Real_Sequence such that

         A7: for n holds X[n, (s . n)] from FUNCT_2:sch 3( A2);

        

         A8: ( rng s) c= (( dom f) \ {x0}) by A7, Th6;

        

         A9: ( lim s) = x0 by A7, Th6;

        let g1,g2 be Real such that

         A10: for seq st seq is convergent & ( lim seq) = x0 & ( rng seq) c= (( dom f) \ {x0}) holds (f /* seq) is convergent & ( lim (f /* seq)) = g1 and

         A11: for seq st seq is convergent & ( lim seq) = x0 & ( rng seq) c= (( dom f) \ {x0}) holds (f /* seq) is convergent & ( lim (f /* seq)) = g2;

        

         A12: s is convergent by A7, Th6;

        then ( lim (f /* s)) = g1 by A9, A8, A10;

        hence thesis by A12, A9, A8, A11;

      end;

    end

    theorem :: LIMFUNC3:28

    f is_convergent_in x0 implies (( lim (f,x0)) = g iff for g1 st 0 < g1 holds ex g2 st 0 < g2 & for r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) holds |.((f . r1) - g).| < g1)

    proof

      assume

       A1: f is_convergent_in x0;

      thus ( lim (f,x0)) = g implies for g1 st 0 < g1 holds ex g2 st 0 < g2 & for r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) holds |.((f . r1) - g).| < g1

      proof

        assume that

         A2: ( lim (f,x0)) = g and

         A3: ex g1 st 0 < g1 & for g2 st 0 < g2 holds ex r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) & g1 <= |.((f . r1) - g).|;

        consider g1 such that

         A4: 0 < g1 and

         A5: for g2 st 0 < g2 holds ex r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) & g1 <= |.((f . r1) - g).| by A3;

        defpred X[ Element of NAT , Real] means 0 < |.(x0 - $2).| & |.(x0 - $2).| < (1 / ($1 + 1)) & $2 in ( dom f) & |.((f . $2) - g).| >= g1;

        

         A6: for n holds ex r1 be Element of REAL st X[n, r1]

        proof

          let n;

          consider r1 such that

           A7: X[n, r1] by A5, XREAL_1: 139;

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

          take r1;

          thus thesis by A7;

        end;

        consider s be Real_Sequence such that

         A8: for n holds X[n, (s . n)] from FUNCT_2:sch 3( A6);

        

         A9: ( rng s) c= (( dom f) \ {x0}) by A8, Th2;

        

         A10: ( lim s) = x0 by A8, Th2;

        

         A11: s is convergent by A8, Th2;

        then

         A12: ( lim (f /* s)) = g by A1, A2, A10, A9, Def4;

        (f /* s) is convergent by A1, A11, A10, A9;

        then

        consider n be Nat such that

         A13: for k be Nat st n <= k holds |.(((f /* s) . k) - g).| < g1 by A4, A12, SEQ_2:def 7;

        

         A14: |.(((f /* s) . n) - g).| < g1 by A13;

        

         A15: n in NAT by ORDINAL1:def 12;

        ( rng s) c= ( dom f) by A8, Th2;

        then |.((f . (s . n)) - g).| < g1 by A14, FUNCT_2: 108, A15;

        hence contradiction by A8, A15;

      end;

      assume

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

      reconsider g as Real;

      now

        let s be Real_Sequence;

        assume that

         A17: s is convergent and

         A18: ( lim s) = x0 and

         A19: ( rng s) c= (( dom f) \ {x0});

         A20:

        now

          let g1 be Real;

          assume

           A21: 0 < g1;

          consider g2 such that

           A22: 0 < g2 and

           A23: for r1 st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in ( dom f) holds |.((f . r1) - g).| < g1 by A16, A21;

          consider n such that

           A24: for k st n <= k holds 0 < |.(x0 - (s . k)).| & |.(x0 - (s . k)).| < g2 & (s . k) in ( dom f) by A17, A18, A19, A22, Th3;

          reconsider n as Nat;

          take n;

          let k be Nat;

          

           A25: k in NAT by ORDINAL1:def 12;

          assume

           A26: n <= k;

          then

           A27: |.(x0 - (s . k)).| < g2 by A24, A25;

          

           A28: (s . k) in ( dom f) by A24, A26, A25;

           0 < |.(x0 - (s . k)).| by A24, A26, A25;

          then |.((f . (s . k)) - g).| < g1 by A23, A27, A28;

          hence |.(((f /* s) . k) - g).| < g1 by A19, FUNCT_2: 108, XBOOLE_1: 1, A25;

        end;

        hence (f /* s) is convergent by SEQ_2:def 6;

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

      end;

      hence thesis by A1, Def4;

    end;

    theorem :: LIMFUNC3:29

    

     Th29: f is_convergent_in x0 implies f is_left_convergent_in x0 & f is_right_convergent_in x0 & ( lim_left (f,x0)) = ( lim_right (f,x0)) & ( lim (f,x0)) = ( lim_left (f,x0)) & ( lim (f,x0)) = ( lim_right (f,x0))

    proof

      assume

       A1: f is_convergent_in x0;

       A2:

      now

        let s be Real_Sequence;

        assume that

         A3: s is convergent and

         A4: ( lim s) = x0 and

         A5: ( rng s) c= (( dom f) /\ ( right_open_halfline x0));

        ( rng s) c= (( dom f) \ {x0}) by A5, Th1;

        hence (f /* s) is convergent & ( lim (f /* s)) = ( lim (f,x0)) by A1, A3, A4, Def4;

      end;

       A6:

      now

        let s be Real_Sequence;

        assume that

         A7: s is convergent and

         A8: ( lim s) = x0 and

         A9: ( rng s) c= (( dom f) /\ ( left_open_halfline x0));

        ( rng s) c= (( dom f) \ {x0}) by A9, Th1;

        hence (f /* s) is convergent & ( lim (f /* s)) = ( lim (f,x0)) by A1, A7, A8, Def4;

      end;

      

       A10: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) by A1;

      then for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom f) by Th8;

      hence f is_left_convergent_in x0 by A6, LIMFUNC2:def 1;

      then

       A11: ( lim_left (f,x0)) = ( lim (f,x0)) by A6, LIMFUNC2:def 7;

      for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom f) by A10, Th8;

      hence f is_right_convergent_in x0 by A2, LIMFUNC2:def 4;

      hence thesis by A11, A2, LIMFUNC2:def 8;

    end;

    theorem :: LIMFUNC3:30

    f is_left_convergent_in x0 & f is_right_convergent_in x0 & ( lim_left (f,x0)) = ( lim_right (f,x0)) implies f is_convergent_in x0 & ( lim (f,x0)) = ( lim_left (f,x0)) & ( lim (f,x0)) = ( lim_right (f,x0))

    proof

      assume that

       A1: f is_left_convergent_in x0 and

       A2: f is_right_convergent_in x0 and

       A3: ( lim_left (f,x0)) = ( lim_right (f,x0));

       A4:

      now

        let s be Real_Sequence such that

         A5: s is convergent and

         A6: ( lim s) = x0 and

         A7: ( rng s) c= (( dom f) \ {x0});

        now

          per cases ;

            suppose ex k st for n st k <= n holds (s . n) < x0;

            then

            consider k such that

             A8: for n st k <= n holds (s . n) < x0;

            

             A9: ( rng s) c= ( dom f) by A7, XBOOLE_1: 1;

            

             A10: ( rng (s ^\ k)) c= (( dom f) /\ ( left_open_halfline x0))

            proof

              let x be object;

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

              then

              consider n such that

               A11: ((s ^\ k) . n) = x by FUNCT_2: 113;

              (s . (n + k)) < x0 by A8, NAT_1: 12;

              then (s . (n + k)) in { g1 : g1 < x0 };

              then (s . (n + k)) in ( left_open_halfline x0) by XXREAL_1: 229;

              then

               A12: x in ( left_open_halfline x0) by A11, NAT_1:def 3;

              (s . (n + k)) in ( rng s) by VALUED_0: 28;

              then x in ( rng s) by A11, NAT_1:def 3;

              hence thesis by A9, A12, XBOOLE_0:def 4;

            end;

            

             A13: (f /* (s ^\ k)) = ((f /* s) ^\ k) by A7, VALUED_0: 27, XBOOLE_1: 1;

            

             A14: ( lim (s ^\ k)) = x0 by A5, A6, SEQ_4: 20;

            then

             A15: (f /* (s ^\ k)) is convergent by A1, A3, A5, A10, LIMFUNC2:def 7;

            hence (f /* s) is convergent by A13, SEQ_4: 21;

            ( lim (f /* (s ^\ k))) = ( lim_left (f,x0)) by A1, A5, A14, A10, LIMFUNC2:def 7;

            hence ( lim (f /* s)) = ( lim_left (f,x0)) by A15, A13, SEQ_4: 22;

          end;

            suppose

             A16: for k holds ex n st k <= n & (s . n) >= x0;

            now

              per cases ;

                suppose ex k st for n st k <= n holds x0 < (s . n);

                then

                consider k such that

                 A17: for n st k <= n holds (s . n) > x0;

                

                 A18: ( rng s) c= ( dom f) by A7, XBOOLE_1: 1;

                

                 A19: ( rng (s ^\ k)) c= (( dom f) /\ ( right_open_halfline x0))

                proof

                  let x be object;

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

                  then

                  consider n such that

                   A20: ((s ^\ k) . n) = x by FUNCT_2: 113;

                  x0 < (s . (n + k)) by A17, NAT_1: 12;

                  then (s . (n + k)) in { g1 : x0 < g1 };

                  then (s . (n + k)) in ( right_open_halfline x0) by XXREAL_1: 230;

                  then

                   A21: x in ( right_open_halfline x0) by A20, NAT_1:def 3;

                  (s . (n + k)) in ( rng s) by VALUED_0: 28;

                  then x in ( rng s) by A20, NAT_1:def 3;

                  hence thesis by A18, A21, XBOOLE_0:def 4;

                end;

                

                 A22: (f /* (s ^\ k)) = ((f /* s) ^\ k) by A7, VALUED_0: 27, XBOOLE_1: 1;

                

                 A23: ( lim (s ^\ k)) = x0 by A5, A6, SEQ_4: 20;

                then

                 A24: (f /* (s ^\ k)) is convergent by A2, A3, A5, A19, LIMFUNC2:def 8;

                hence (f /* s) is convergent by A22, SEQ_4: 21;

                ( lim (f /* (s ^\ k))) = ( lim_left (f,x0)) by A2, A3, A5, A23, A19, LIMFUNC2:def 8;

                hence ( lim (f /* s)) = ( lim_left (f,x0)) by A24, A22, SEQ_4: 22;

              end;

                suppose

                 A25: for k holds ex n st k <= n & x0 >= (s . n);

                set GR = ( lim_left (f,x0));

                defpred P[ set, set] means for n, m st $1 = n & $2 = m holds n < m & (s . m) < x0 & for k st n < k & (s . k) < x0 holds m <= k;

                defpred X[ Nat, set, set] means P[$2, $3];

                defpred X[ Nat] means (s . $1) < x0;

                 A26:

                now

                  let k;

                  consider n such that

                   A27: k <= n and

                   A28: (s . n) <= x0 by A25;

                  take n;

                  thus k <= n by A27;

                  (s . n) in ( rng s) by VALUED_0: 28;

                  then not (s . n) in {x0} by A7, XBOOLE_0:def 5;

                  then (s . n) <> x0 by TARSKI:def 1;

                  hence (s . n) < x0 by A28, XXREAL_0: 1;

                end;

                then ex m1 be Element of NAT st 0 <= m1 & (s . m1) < x0;

                then

                 A29: ex m be Nat st X[m];

                consider M be Nat such that

                 A30: X[M] & for n be Nat st X[n] holds M <= n from NAT_1:sch 5( A29);

                reconsider M9 = M as Element of NAT by ORDINAL1:def 12;

                 A31:

                now

                  let n;

                  consider m such that

                   A32: (n + 1) <= m and

                   A33: (s . m) < x0 by A26;

                  take m;

                  thus n < m & (s . m) < x0 by A32, A33, NAT_1: 13;

                end;

                

                 A34: for n be Nat holds for x be Element of NAT holds ex y be Element of NAT st X[n, x, y]

                proof

                  let n be Nat;

                  let x be Element of NAT ;

                  defpred X[ Nat] means x < $1 & (s . $1) < x0;

                  ex m st X[m] by A31;

                  then

                   A35: ex m be Nat st X[m];

                  consider l be Nat such that

                   A36: X[l] & for k be Nat st X[k] holds l <= k from NAT_1:sch 5( A35);

                  take l;

                  l in NAT by ORDINAL1:def 12;

                  hence thesis by A36;

                end;

                consider F be sequence of NAT such that

                 A37: (F . 0 ) = M9 & for n be Nat holds X[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A34);

                

                 A38: ( rng F) c= NAT by RELAT_1:def 19;

                then

                 A39: ( rng F) c= REAL by NUMBERS: 19;

                

                 A40: ( dom F) = NAT by FUNCT_2:def 1;

                then

                reconsider F as Real_Sequence by A39, RELSET_1: 4;

                 A41:

                now

                  let n;

                  (F . n) in ( rng F) by A40, FUNCT_1:def 3;

                  hence (F . n) is Element of NAT by A38;

                end;

                now

                  let n be Nat;

                  

                   A42: n in NAT by ORDINAL1:def 12;

                  

                   A43: (F . (n + 1)) is Element of NAT by A41;

                  (F . n) is Element of NAT by A41, A42;

                  hence (F . n) < (F . (n + 1)) by A37, A43;

                end;

                then

                reconsider F as increasing sequence of NAT by SEQM_3:def 6;

                

                 A44: (s * F) is subsequence of s by VALUED_0:def 17;

                then ( rng (s * F)) c= ( rng s) by VALUED_0: 21;

                then

                 A45: ( rng (s * F)) c= (( dom f) \ {x0}) by A7;

                defpred X[ Nat] means (s . $1) < x0 & for m holds (F . m) <> $1;

                

                 A46: for n st (s . n) < x0 holds ex m st (F . m) = n

                proof

                  assume ex n st X[n];

                  then

                   A47: ex n be Nat st X[n];

                  consider M1 be Nat such that

                   A48: X[M1] & for n be Nat st X[n] holds M1 <= n from NAT_1:sch 5( A47);

                  defpred X[ Nat] means $1 < M1 & (s . $1) < x0 & ex m st (F . m) = $1;

                  

                   A49: ex n be Nat st X[n]

                  proof

                    take M;

                    

                     A50: M <> M1 by A37, A48;

                    M <= M1 by A30, A48;

                    hence M < M1 by A50, XXREAL_0: 1;

                    thus (s . M) < x0 by A30;

                    take 0 ;

                    thus thesis by A37;

                  end;

                  

                   A51: for n be Nat st X[n] holds n <= M1;

                  consider MX be Nat such that

                   A52: X[MX] & for n be Nat st X[n] holds n <= MX from NAT_1:sch 6( A51, A49);

                  

                   A53: for k st MX < k & k < M1 holds (s . k) >= x0

                  proof

                    given k such that

                     A54: MX < k and

                     A55: k < M1 and

                     A56: (s . k) < x0;

                    now

                      per cases ;

                        suppose ex m st (F . m) = k;

                        hence contradiction by A52, A54, A55, A56;

                      end;

                        suppose for m holds (F . m) <> k;

                        hence contradiction by A48, A55, A56;

                      end;

                    end;

                    hence contradiction;

                  end;

                  consider m such that

                   A57: (F . m) = MX by A52;

                  M1 in NAT by ORDINAL1:def 12;

                  then

                   A58: (F . (m + 1)) <= M1 by A37, A48, A52, A57;

                  

                   A59: (s . (F . (m + 1))) < x0 by A37, A57;

                  

                   A60: MX < (F . (m + 1)) by A37, A57;

                  now

                    assume (F . (m + 1)) <> M1;

                    then (F . (m + 1)) < M1 by A58, XXREAL_0: 1;

                    hence contradiction by A53, A60, A59;

                  end;

                  hence contradiction by A48;

                end;

                defpred X[ Nat] means (s . $1) > x0;

                 A61:

                now

                  let k;

                  consider n such that

                   A62: k <= n and

                   A63: (s . n) >= x0 by A16;

                  take n;

                  thus k <= n by A62;

                  (s . n) in ( rng s) by VALUED_0: 28;

                  then not (s . n) in {x0} by A7, XBOOLE_0:def 5;

                  then (s . n) <> x0 by TARSKI:def 1;

                  hence (s . n) > x0 by A63, XXREAL_0: 1;

                end;

                then ex mn be Element of NAT st 0 <= mn & (s . mn) > x0;

                then

                 A64: ex m be Nat st X[m];

                consider N be Nat such that

                 A65: X[N] & for n be Nat st X[n] holds N <= n from NAT_1:sch 5( A64);

                defpred X[ Nat] means ((s * F) . $1) < x0;

                

                 A66: for k be Nat st X[k] holds X[(k + 1)]

                proof

                  let k be Nat such that ((s * F) . k) < x0;

                   P[(F . k), (F . (k + 1))] by A37;

                  then (s . (F . (k + 1))) < x0;

                  hence thesis by FUNCT_2: 15;

                end;

                

                 A67: X[ 0 ] by A30, A37, FUNCT_2: 15;

                

                 A68: for k be Nat holds X[k] from NAT_1:sch 2( A67, A66);

                

                 A69: ( rng (s * F)) c= (( dom f) /\ ( left_open_halfline x0))

                proof

                  let x be object;

                  assume

                   A70: x in ( rng (s * F));

                  then

                  consider n such that

                   A71: ((s * F) . n) = x by FUNCT_2: 113;

                  ((s * F) . n) < x0 by A68;

                  then x in { g1 : g1 < x0 } by A71;

                  then

                   A72: x in ( left_open_halfline x0) by XXREAL_1: 229;

                  x in ( dom f) by A45, A70, XBOOLE_0:def 5;

                  hence thesis by A72, XBOOLE_0:def 4;

                end;

                defpred P[ set, set] means for n, m st $1 = n & $2 = m holds n < m & (s . m) > x0 & for k st n < k & (s . k) > x0 holds m <= k;

                defpred X[ Nat, set, set] means P[$2, $3];

                

                 A73: (s * F) is convergent by A5, A44, SEQ_4: 16;

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

                 A74:

                now

                  let n;

                  consider m such that

                   A75: (n + 1) <= m and

                   A76: (s . m) > x0 by A61;

                  take m;

                  thus n < m & (s . m) > x0 by A75, A76, NAT_1: 13;

                end;

                

                 A77: for n be Nat holds for x be Element of NAT holds ex y be Element of NAT st X[n, x, y]

                proof

                  let n be Nat;

                  let x be Element of NAT ;

                  defpred X[ Nat] means x < $1 & (s . $1) > x0;

                  ex m st X[m] by A74;

                  then

                   A78: ex m be Nat st X[m];

                  consider l be Nat such that

                   A79: X[l] & for k be Nat st X[k] holds l <= k from NAT_1:sch 5( A78);

                  take l;

                  l in NAT by ORDINAL1:def 12;

                  hence thesis by A79;

                end;

                consider G be sequence of NAT such that

                 A80: (G . 0 ) = N9 & for n be Nat holds X[n, (G . n), (G . (n + 1))] from RECDEF_1:sch 2( A77);

                

                 A81: ( rng G) c= NAT by RELAT_1:def 19;

                then

                 A82: ( rng G) c= REAL by NUMBERS: 19;

                

                 A83: ( dom G) = NAT by FUNCT_2:def 1;

                then

                reconsider G as Real_Sequence by A82, RELSET_1: 4;

                 A84:

                now

                  let n;

                  (G . n) in ( rng G) by A83, FUNCT_1:def 3;

                  hence (G . n) is Element of NAT by A81;

                end;

                now

                  let n be Nat;

                  

                   A85: n in NAT by ORDINAL1:def 12;

                  

                   A86: (G . (n + 1)) is Element of NAT by A84;

                  (G . n) is Element of NAT by A84, A85;

                  hence (G . n) < (G . (n + 1)) by A80, A86;

                end;

                then

                reconsider G as increasing sequence of NAT by SEQM_3:def 6;

                

                 A87: (s * G) is subsequence of s by VALUED_0:def 17;

                then ( rng (s * G)) c= ( rng s) by VALUED_0: 21;

                then

                 A88: ( rng (s * G)) c= (( dom f) \ {x0}) by A7;

                

                 A89: ( lim (s * F)) = x0 by A5, A6, A44, SEQ_4: 17;

                then

                 A90: ( lim (f /* (s * F))) = ( lim_left (f,x0)) by A1, A73, A69, LIMFUNC2:def 7;

                

                 A91: (f /* (s * F)) is convergent by A1, A3, A73, A89, A69, LIMFUNC2:def 7;

                

                 A92: (s * G) is convergent by A5, A87, SEQ_4: 16;

                defpred X[ Nat] means (s . $1) > x0 & for m holds (G . m) <> $1;

                

                 A93: for n st (s . n) > x0 holds ex m st (G . m) = n

                proof

                  assume ex n st X[n];

                  then

                   A94: ex n be Nat st X[n];

                  consider N1 be Nat such that

                   A95: X[N1] & for n be Nat st X[n] holds N1 <= n from NAT_1:sch 5( A94);

                  defpred X[ Nat] means $1 < N1 & (s . $1) > x0 & ex m st (G . m) = $1;

                  

                   A96: ex n be Nat st X[n]

                  proof

                    take N;

                    

                     A97: N <> N1 by A80, A95;

                    N <= N1 by A65, A95;

                    hence N < N1 by A97, XXREAL_0: 1;

                    thus (s . N) > x0 by A65;

                    take 0 ;

                    thus thesis by A80;

                  end;

                  

                   A98: for n be Nat st X[n] holds n <= N1;

                  consider NX be Nat such that

                   A99: X[NX] & for n be Nat st X[n] holds n <= NX from NAT_1:sch 6( A98, A96);

                  

                   A100: for k st NX < k & k < N1 holds (s . k) <= x0

                  proof

                    given k such that

                     A101: NX < k and

                     A102: k < N1 and

                     A103: (s . k) > x0;

                    now

                      per cases ;

                        suppose ex m st (G . m) = k;

                        hence contradiction by A99, A101, A102, A103;

                      end;

                        suppose for m holds (G . m) <> k;

                        hence contradiction by A95, A102, A103;

                      end;

                    end;

                    hence contradiction;

                  end;

                  consider m such that

                   A104: (G . m) = NX by A99;

                  N1 in NAT by ORDINAL1:def 12;

                  then

                   A105: (G . (m + 1)) <= N1 by A80, A95, A99, A104;

                  

                   A106: (s . (G . (m + 1))) > x0 by A80, A104;

                  

                   A107: NX < (G . (m + 1)) by A80, A104;

                  now

                    assume (G . (m + 1)) <> N1;

                    then (G . (m + 1)) < N1 by A105, XXREAL_0: 1;

                    hence contradiction by A100, A107, A106;

                  end;

                  hence contradiction by A95;

                end;

                defpred X[ Nat] means ((s * G) . $1) > x0;

                

                 A108: for k be Nat st X[k] holds X[(k + 1)]

                proof

                  let k be Nat such that ((s * G) . k) > x0;

                   P[(G . k), (G . (k + 1))] by A80;

                  then (s . (G . (k + 1))) > x0;

                  hence thesis by FUNCT_2: 15;

                end;

                

                 A109: X[ 0 ] by A65, A80, FUNCT_2: 15;

                

                 A110: for k be Nat holds X[k] from NAT_1:sch 2( A109, A108);

                

                 A111: ( rng (s * G)) c= (( dom f) /\ ( right_open_halfline x0))

                proof

                  let x be object;

                  assume

                   A112: x in ( rng (s * G));

                  then

                  consider n such that

                   A113: ((s * G) . n) = x by FUNCT_2: 113;

                  ((s * G) . n) > x0 by A110;

                  then x in { g1 : x0 < g1 } by A113;

                  then

                   A114: x in ( right_open_halfline x0) by XXREAL_1: 230;

                  x in ( dom f) by A88, A112, XBOOLE_0:def 5;

                  hence thesis by A114, XBOOLE_0:def 4;

                end;

                

                 A115: ( lim (s * G)) = x0 by A5, A6, A87, SEQ_4: 17;

                then

                 A116: ( lim (f /* (s * G))) = ( lim_left (f,x0)) by A2, A3, A92, A111, LIMFUNC2:def 8;

                

                 A117: (f /* (s * G)) is convergent by A2, A3, A92, A115, A111, LIMFUNC2:def 8;

                 A118:

                now

                  let r be Real;

                  assume

                   A119: 0 < r;

                  then

                  consider n1 be Nat such that

                   A120: for k be Nat st n1 <= k holds |.(((f /* (s * F)) . k) - GR).| < r by A91, A90, SEQ_2:def 7;

                  consider n2 be Nat such that

                   A121: for k be Nat st n2 <= k holds |.(((f /* (s * G)) . k) - GR).| < r by A117, A116, A119, SEQ_2:def 7;

                  reconsider n = ( max ((F . n1),(G . n2))) as Nat;

                  take n;

                  let k be Nat;

                  

                   A122: k in NAT by ORDINAL1:def 12;

                  assume

                   A123: n <= k;

                  (s . k) in ( rng s) by VALUED_0: 28;

                  then not (s . k) in {x0} by A7, XBOOLE_0:def 5;

                  then

                   A124: (s . k) <> x0 by TARSKI:def 1;

                  now

                    per cases by A124, XXREAL_0: 1;

                      suppose (s . k) < x0;

                      then

                      consider l be Element of NAT such that

                       A125: k = (F . l) by A46, A122;

                      (F . n1) <= n by XXREAL_0: 25;

                      then (F . n1) <= k by A123, XXREAL_0: 2;

                      then l >= n1 by A125, SEQM_3: 1;

                      then |.(((f /* (s * F)) . l) - GR).| < r by A120;

                      then |.((f . ((s * F) . l)) - GR).| < r by A45, FUNCT_2: 108, XBOOLE_1: 1;

                      then |.((f . (s . k)) - GR).| < r by A125, FUNCT_2: 15;

                      hence |.(((f /* s) . k) - GR).| < r by A7, FUNCT_2: 108, XBOOLE_1: 1, A122;

                    end;

                      suppose (s . k) > x0;

                      then

                      consider l be Element of NAT such that

                       A126: k = (G . l) by A93, A122;

                      (G . n2) <= n by XXREAL_0: 25;

                      then (G . n2) <= k by A123, XXREAL_0: 2;

                      then l >= n2 by A126, SEQM_3: 1;

                      then |.(((f /* (s * G)) . l) - GR).| < r by A121;

                      then |.((f . ((s * G) . l)) - GR).| < r by A88, FUNCT_2: 108, XBOOLE_1: 1;

                      then |.((f . (s . k)) - GR).| < r by A126, FUNCT_2: 15;

                      hence |.(((f /* s) . k) - GR).| < r by A7, FUNCT_2: 108, XBOOLE_1: 1, A122;

                    end;

                  end;

                  hence |.(((f /* s) . k) - GR).| < r;

                end;

                hence (f /* s) is convergent by SEQ_2:def 6;

                hence ( lim (f /* s)) = ( lim_left (f,x0)) by A118, SEQ_2:def 7;

              end;

            end;

            hence (f /* s) is convergent & ( lim (f /* s)) = ( lim_left (f,x0));

          end;

        end;

        hence (f /* s) is convergent & ( lim (f /* s)) = ( lim_left (f,x0));

      end;

      now

        let r1, r2;

        assume that

         A127: r1 < x0 and

         A128: x0 < r2;

        consider g1 such that

         A129: r1 < g1 and

         A130: g1 < x0 and

         A131: g1 in ( dom f) by A1, A127, LIMFUNC2:def 1;

        consider g2 such that

         A132: g2 < r2 and

         A133: x0 < g2 and

         A134: g2 in ( dom f) by A2, A128, LIMFUNC2:def 4;

        take g1;

        take g2;

        thus r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) by A129, A130, A131, A132, A133, A134;

      end;

      hence f is_convergent_in x0 by A4;

      hence thesis by A3, A4, Def4;

    end;

    theorem :: LIMFUNC3:31

    

     Th31: f is_convergent_in x0 implies (r (#) f) is_convergent_in x0 & ( lim ((r (#) f),x0)) = (r * ( lim (f,x0)))

    proof

      assume

       A1: f is_convergent_in x0;

       A2:

      now

        let seq;

        assume that

         A3: seq is convergent and

         A4: ( lim seq) = x0 and

         A5: ( rng seq) c= (( dom (r (#) f)) \ {x0});

        

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

        then

         A7: (r (#) (f /* seq)) = ((r (#) f) /* seq) by RFUNCT_2: 9, XBOOLE_1: 1;

        

         A8: (f /* seq) is convergent by A1, A3, A4, A6;

        then (r (#) (f /* seq)) is convergent by SEQ_2: 7;

        hence ((r (#) f) /* seq) is convergent by A6, RFUNCT_2: 9, XBOOLE_1: 1;

        ( lim (f /* seq)) = ( lim (f,x0)) by A1, A3, A4, A6, Def4;

        hence ( lim ((r (#) f) /* seq)) = (r * ( lim (f,x0))) by A8, A7, SEQ_2: 8;

      end;

      now

        let r1, r2;

        assume that

         A9: r1 < x0 and

         A10: x0 < r2;

        consider g1, g2 such that

         A11: r1 < g1 and

         A12: g1 < x0 and

         A13: g1 in ( dom f) and

         A14: g2 < r2 and

         A15: x0 < g2 and

         A16: g2 in ( dom f) by A1, A9, A10;

        take g1;

        take g2;

        thus r1 < g1 & g1 < x0 & g1 in ( dom (r (#) f)) & g2 < r2 & x0 < g2 & g2 in ( dom (r (#) f)) by A11, A12, A13, A14, A15, A16, VALUED_1:def 5;

      end;

      hence (r (#) f) is_convergent_in x0 by A2;

      hence thesis by A2, Def4;

    end;

    theorem :: LIMFUNC3:32

    

     Th32: f is_convergent_in x0 implies ( - f) is_convergent_in x0 & ( lim (( - f),x0)) = ( - ( lim (f,x0)))

    proof

      assume

       A1: f is_convergent_in x0;

      thus ( - f) is_convergent_in x0 by A1, Th31;

      

      thus ( lim (( - f),x0)) = (( - 1) * ( lim (f,x0))) by A1, Th31

      .= ( - ( lim (f,x0)));

    end;

    theorem :: LIMFUNC3:33

    

     Th33: f1 is_convergent_in x0 & f2 is_convergent_in x0 & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f1 + f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 + f2))) implies (f1 + f2) is_convergent_in x0 & ( lim ((f1 + f2),x0)) = (( lim (f1,x0)) + ( lim (f2,x0)))

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_convergent_in x0 and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f1 + f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 + f2));

       A4:

      now

        let seq;

        assume that

         A5: seq is convergent and

         A6: ( lim seq) = x0 and

         A7: ( rng seq) c= (( dom (f1 + f2)) \ {x0});

        

         A8: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by A7, Lm4;

        

         A9: ( rng seq) c= (( dom f1) \ {x0}) by A7, Lm4;

        

         A10: ( rng seq) c= (( dom f2) \ {x0}) by A7, Lm4;

        then

         A11: ( lim (f2 /* seq)) = ( lim (f2,x0)) by A2, A5, A6, Def4;

        

         A12: (f2 /* seq) is convergent by A2, A5, A6, A10;

        ( rng seq) c= ( dom (f1 + f2)) by A7, Lm4;

        then

         A13: ((f1 /* seq) + (f2 /* seq)) = ((f1 + f2) /* seq) by A8, RFUNCT_2: 8;

        

         A14: (f1 /* seq) is convergent by A1, A5, A6, A9;

        hence ((f1 + f2) /* seq) is convergent by A12, A13, SEQ_2: 5;

        ( lim (f1 /* seq)) = ( lim (f1,x0)) by A1, A5, A6, A9, Def4;

        hence ( lim ((f1 + f2) /* seq)) = (( lim (f1,x0)) + ( lim (f2,x0))) by A14, A12, A11, A13, SEQ_2: 6;

      end;

      hence (f1 + f2) is_convergent_in x0 by A3;

      hence thesis by A4, Def4;

    end;

    theorem :: LIMFUNC3:34

    f1 is_convergent_in x0 & f2 is_convergent_in x0 & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f1 - f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 - f2))) implies (f1 - f2) is_convergent_in x0 & ( lim ((f1 - f2),x0)) = (( lim (f1,x0)) - ( lim (f2,x0)))

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_convergent_in x0 and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f1 - f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 - f2));

      

       A4: ( - f2) is_convergent_in x0 by A2, Th32;

      hence (f1 - f2) is_convergent_in x0 by A1, A3, Th33;

      

      thus ( lim ((f1 - f2),x0)) = (( lim (f1,x0)) + ( lim (( - f2),x0))) by A1, A3, A4, Th33

      .= (( lim (f1,x0)) + ( - ( lim (f2,x0)))) by A2, Th32

      .= (( lim (f1,x0)) - ( lim (f2,x0)));

    end;

    theorem :: LIMFUNC3:35

    f is_convergent_in x0 & (f " { 0 }) = {} & ( lim (f,x0)) <> 0 implies (f ^ ) is_convergent_in x0 & ( lim ((f ^ ),x0)) = (( lim (f,x0)) " )

    proof

      assume that

       A1: f is_convergent_in x0 and

       A2: (f " { 0 }) = {} and

       A3: ( lim (f,x0)) <> 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 convergent and

         A7: ( lim seq) = x0 and

         A8: ( rng seq) c= (( dom (f ^ )) \ {x0});

        

         A9: ( lim (f /* seq)) = ( lim (f,x0)) by A1, A4, A6, A7, A8, Def4;

        

         A10: ((f /* seq) " ) = ((f ^ ) /* seq) by A8, RFUNCT_2: 12, XBOOLE_1: 1;

        

         A11: ( rng seq) c= ( dom f) by A4, A8, XBOOLE_1: 1;

        

         A12: (f /* seq) is convergent by A1, A4, A6, A7, A8;

        hence ((f ^ ) /* seq) is convergent by A3, A4, A9, A11, A10, RFUNCT_2: 11, SEQ_2: 21;

        thus ( lim ((f ^ ) /* seq)) = (( lim (f,x0)) " ) by A3, A4, A12, A9, A11, A10, RFUNCT_2: 11, SEQ_2: 22;

      end;

      for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f ^ )) & g2 < r2 & x0 < g2 & g2 in ( dom (f ^ )) by A1, A4;

      hence (f ^ ) is_convergent_in x0 by A5;

      hence thesis by A5, Def4;

    end;

    theorem :: LIMFUNC3:36

    f is_convergent_in x0 implies ( abs f) is_convergent_in x0 & ( lim (( abs f),x0)) = |.( lim (f,x0)).|

    proof

      assume

       A1: f is_convergent_in x0;

       A2:

      now

        let seq;

        assume that

         A3: seq is convergent and

         A4: ( lim seq) = x0 and

         A5: ( rng seq) c= (( dom ( abs f)) \ {x0});

        

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

        then ( rng seq) c= ( dom f) by XBOOLE_1: 1;

        then

         A7: ( abs (f /* seq)) = (( abs f) /* seq) by RFUNCT_2: 10;

        

         A8: (f /* seq) is convergent by A1, A3, A4, A6;

        hence (( abs f) /* seq) is convergent by A7;

        ( lim (f /* seq)) = ( lim (f,x0)) by A1, A3, A4, A6, Def4;

        hence ( lim (( abs f) /* seq)) = |.( lim (f,x0)).| by A8, A7, SEQ_4: 14;

      end;

      now

        let r1, r2;

        assume that

         A9: r1 < x0 and

         A10: x0 < r2;

        consider g1, g2 such that

         A11: r1 < g1 and

         A12: g1 < x0 and

         A13: g1 in ( dom f) and

         A14: g2 < r2 and

         A15: x0 < g2 and

         A16: g2 in ( dom f) by A1, A9, A10;

        take g1;

        take g2;

        thus r1 < g1 & g1 < x0 & g1 in ( dom ( abs f)) & g2 < r2 & x0 < g2 & g2 in ( dom ( abs f)) by A11, A12, A13, A14, A15, A16, VALUED_1:def 11;

      end;

      hence ( abs f) is_convergent_in x0 by A2;

      hence thesis by A2, Def4;

    end;

    theorem :: LIMFUNC3:37

    

     Th37: f is_convergent_in x0 & ( lim (f,x0)) <> 0 & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) & (f . g1) <> 0 & (f . g2) <> 0 ) implies (f ^ ) is_convergent_in x0 & ( lim ((f ^ ),x0)) = (( lim (f,x0)) " )

    proof

      assume that

       A1: f is_convergent_in x0 and

       A2: ( lim (f,x0)) <> 0 and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) & (f . g1) <> 0 & (f . g2) <> 0 ;

      

       A4: (( dom f) \ (f " { 0 })) = ( dom (f ^ )) by RFUNCT_1:def 2;

       A5:

      now

        let seq;

        assume that

         A6: seq is convergent and

         A7: ( lim seq) = x0 and

         A8: ( rng seq) c= (( dom (f ^ )) \ {x0});

        

         A9: (f /* seq) is non-zero by A8, RFUNCT_2: 11, XBOOLE_1: 1;

        ( rng seq) c= ( dom (f ^ )) by A8, XBOOLE_1: 1;

        then

         A10: ( rng seq) c= ( dom f) by A4, XBOOLE_1: 1;

        now

          let x be object;

          assume

           A11: x in ( rng seq);

          then not x in {x0} by A8, XBOOLE_0:def 5;

          hence x in (( dom f) \ {x0}) by A10, A11, XBOOLE_0:def 5;

        end;

        then

         A12: ( rng seq) c= (( dom f) \ {x0});

        then

         A13: ( lim (f /* seq)) = ( lim (f,x0)) by A1, A6, A7, Def4;

        

         A14: ((f /* seq) " ) = ((f ^ ) /* seq) by A8, RFUNCT_2: 12, XBOOLE_1: 1;

        

         A15: (f /* seq) is convergent by A1, A6, A7, A12;

        hence ((f ^ ) /* seq) is convergent by A2, A13, A9, A14, SEQ_2: 21;

        thus ( lim ((f ^ ) /* seq)) = (( lim (f,x0)) " ) by A2, A15, A13, A9, A14, SEQ_2: 22;

      end;

      now

        let r1, r2;

        assume that

         A16: r1 < x0 and

         A17: x0 < r2;

        consider g1, g2 such that

         A18: r1 < g1 and

         A19: g1 < x0 and

         A20: g1 in ( dom f) and

         A21: g2 < r2 and

         A22: x0 < g2 and

         A23: g2 in ( dom f) and

         A24: (f . g1) <> 0 and

         A25: (f . g2) <> 0 by A3, A16, A17;

        take g1, g2;

         not (f . g2) in { 0 } by A25, TARSKI:def 1;

        then

         A26: not g2 in (f " { 0 }) by FUNCT_1:def 7;

         not (f . g1) in { 0 } by A24, TARSKI:def 1;

        then not g1 in (f " { 0 }) by FUNCT_1:def 7;

        hence r1 < g1 & g1 < x0 & g1 in ( dom (f ^ )) & g2 < r2 & x0 < g2 & g2 in ( dom (f ^ )) by A4, A18, A19, A20, A21, A22, A23, A26, XBOOLE_0:def 5;

      end;

      hence (f ^ ) is_convergent_in x0 by A5;

      hence thesis by A5, Def4;

    end;

    theorem :: LIMFUNC3:38

    

     Th38: f1 is_convergent_in x0 & f2 is_convergent_in x0 & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f1 (#) f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 (#) f2))) implies (f1 (#) f2) is_convergent_in x0 & ( lim ((f1 (#) f2),x0)) = (( lim (f1,x0)) * ( lim (f2,x0)))

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_convergent_in x0 and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f1 (#) f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 (#) f2));

       A4:

      now

        let seq;

        assume that

         A5: seq is convergent and

         A6: ( lim seq) = x0 and

         A7: ( rng seq) c= (( dom (f1 (#) f2)) \ {x0});

        

         A8: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by A7, Lm2;

        

         A9: ( rng seq) c= (( dom f1) \ {x0}) by A7, Lm2;

        

         A10: ( rng seq) c= (( dom f2) \ {x0}) by A7, Lm2;

        then

         A11: ( lim (f2 /* seq)) = ( lim (f2,x0)) by A2, A5, A6, Def4;

        

         A12: (f2 /* seq) is convergent by A2, A5, A6, A10;

        ( rng seq) c= ( dom (f1 (#) f2)) by A7, Lm2;

        then

         A13: ((f1 /* seq) (#) (f2 /* seq)) = ((f1 (#) f2) /* seq) by A8, RFUNCT_2: 8;

        

         A14: (f1 /* seq) is convergent by A1, A5, A6, A9;

        hence ((f1 (#) f2) /* seq) is convergent by A12, A13, SEQ_2: 14;

        ( lim (f1 /* seq)) = ( lim (f1,x0)) by A1, A5, A6, A9, Def4;

        hence ( lim ((f1 (#) f2) /* seq)) = (( lim (f1,x0)) * ( lim (f2,x0))) by A14, A12, A11, A13, SEQ_2: 15;

      end;

      hence (f1 (#) f2) is_convergent_in x0 by A3;

      hence thesis by A4, Def4;

    end;

    theorem :: LIMFUNC3:39

    f1 is_convergent_in x0 & f2 is_convergent_in x0 & ( lim (f2,x0)) <> 0 & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f1 / f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 / f2))) implies (f1 / f2) is_convergent_in x0 & ( lim ((f1 / f2),x0)) = (( lim (f1,x0)) / ( lim (f2,x0)))

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_convergent_in x0 and

       A3: ( lim (f2,x0)) <> 0 and

       A4: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f1 / f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 / f2));

       A5:

      now

        let r1, r2;

        assume that

         A6: r1 < x0 and

         A7: x0 < r2;

        consider g1, g2 such that

         A8: r1 < g1 and

         A9: g1 < x0 and

         A10: g1 in ( dom (f1 / f2)) and

         A11: g2 < r2 and

         A12: x0 < g2 and

         A13: g2 in ( dom (f1 / f2)) by A4, A6, A7;

        take g1;

        take g2;

        thus r1 < g1 & g1 < x0 by A8, A9;

        

         A14: ( dom (f1 / f2)) = (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by RFUNCT_1:def 1;

        then g2 in (( dom f2) \ (f2 " { 0 })) by A13, XBOOLE_0:def 4;

        then not g2 in (f2 " { 0 }) by XBOOLE_0:def 5;

        then

         A15: not (f2 . g2) in { 0 } by A13, A14, FUNCT_1:def 7;

        g1 in (( dom f2) \ (f2 " { 0 })) by A10, A14, XBOOLE_0:def 4;

        then not g1 in (f2 " { 0 }) by XBOOLE_0:def 5;

        then not (f2 . g1) in { 0 } by A10, A14, FUNCT_1:def 7;

        hence g1 in ( dom f2) & g2 < r2 & x0 < g2 & g2 in ( dom f2) & (f2 . g1) <> 0 & (f2 . g2) <> 0 by A10, A11, A12, A13, A14, A15, TARSKI:def 1;

      end;

      then

       A16: (f2 ^ ) is_convergent_in x0 by A2, A3, Th37;

      

       A17: (f1 / f2) = (f1 (#) (f2 ^ )) by RFUNCT_1: 31;

      hence (f1 / f2) is_convergent_in x0 by A1, A4, A16, Th38;

      ( lim ((f2 ^ ),x0)) = (( lim (f2,x0)) " ) by A2, A3, A5, Th37;

      

      hence ( lim ((f1 / f2),x0)) = (( lim (f1,x0)) * (( lim (f2,x0)) " )) by A1, A4, A17, A16, Th38

      .= (( lim (f1,x0)) / ( lim (f2,x0))) by XCMPLX_0:def 9;

    end;

    theorem :: LIMFUNC3:40

    f1 is_convergent_in x0 & ( lim (f1,x0)) = 0 & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f1 (#) f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 (#) f2))) & (ex r st 0 < r & (f2 | ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) is bounded) implies (f1 (#) f2) is_convergent_in x0 & ( lim ((f1 (#) f2),x0)) = 0

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: ( lim (f1,x0)) = 0 and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f1 (#) f2)) & g2 < r2 & x0 < g2 & g2 in ( dom (f1 (#) f2));

      given r such that

       A4: 0 < r and

       A5: (f2 | ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) is bounded;

      consider g be Real such that

       A6: for r1 be object st r1 in (( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) /\ ( dom f2)) holds |.(f2 . r1).| <= g by A5, RFUNCT_1: 73;

       A7:

      now

        let s be Real_Sequence;

        assume that

         A8: s is convergent and

         A9: ( lim s) = x0 and

         A10: ( rng s) c= (( dom (f1 (#) f2)) \ {x0});

        consider k such that

         A11: for n st k <= n holds (x0 - r) < (s . n) & (s . n) < (x0 + r) by A4, A8, A9, Th7;

        

         A12: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

        ( rng s) c= (( dom f1) \ {x0}) by A10, Lm2;

        then

         A13: ( rng (s ^\ k)) c= (( dom f1) \ {x0}) by A12;

        

         A14: ( lim (s ^\ k)) = x0 by A8, A9, SEQ_4: 20;

        then

         A15: (f1 /* (s ^\ k)) is convergent by A1, A8, A13;

        

         A16: ( rng s) c= ( dom f2) by A10, Lm2;

        then

         A17: ( rng (s ^\ k)) c= ( dom f2) by A12;

        now

          set t = ( |.g.| + 1);

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

          hence 0 < t;

          let n be Nat;

          

           A18: n in NAT by ORDINAL1:def 12;

          

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

          then (s . (n + k)) < (x0 + r) by A11;

          then

           A20: ((s ^\ k) . n) < (x0 + r) by NAT_1:def 3;

          (x0 - r) < (s . (n + k)) by A11, A19;

          then (x0 - r) < ((s ^\ k) . n) by NAT_1:def 3;

          then ((s ^\ k) . n) in { g1 : (x0 - r) < g1 & g1 < (x0 + r) } by A20;

          then

           A21: ((s ^\ k) . n) in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

          

           A22: ((s ^\ k) . n) in ( rng (s ^\ k)) by VALUED_0: 28;

          then not ((s ^\ k) . n) in {x0} by A13, XBOOLE_0:def 5;

          then ((s ^\ k) . n) in ( ].(x0 - r), (x0 + r).[ \ {x0}) by A21, XBOOLE_0:def 5;

          then ((s ^\ k) . n) in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by A4, Th4;

          then ((s ^\ k) . n) in (( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) /\ ( dom f2)) by A17, A22, XBOOLE_0:def 4;

          then |.(f2 . ((s ^\ k) . n)).| <= g by A6;

          then

           A23: |.((f2 /* (s ^\ k)) . n).| <= g by A16, A12, FUNCT_2: 108, XBOOLE_1: 1, A18;

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

          then g < t by Lm1;

          hence |.((f2 /* (s ^\ k)) . n).| < t by A23, XXREAL_0: 2;

        end;

        then

         A24: (f2 /* (s ^\ k)) is bounded by SEQ_2: 3;

        

         A25: ( rng s) c= ( dom (f1 (#) f2)) by A10, Lm2;

        ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by A10, Lm2;

        then ( rng (s ^\ k)) c= (( dom f1) /\ ( dom f2)) by A25, A12;

        

        then

         A26: ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) = ((f1 (#) f2) /* (s ^\ k)) by RFUNCT_2: 8

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

        

         A27: ( lim (f1 /* (s ^\ k))) = 0 by A1, A2, A8, A14, A13, Def4;

        then

         A28: ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) is convergent by A15, A24, SEQ_2: 25;

        hence ((f1 (#) f2) /* s) is convergent by A26, SEQ_4: 21;

        ( lim ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)))) = 0 by A15, A27, A24, SEQ_2: 26;

        hence ( lim ((f1 (#) f2) /* s)) = 0 by A28, A26, SEQ_4: 22;

      end;

      hence (f1 (#) f2) is_convergent_in x0 by A3;

      hence thesis by A7, Def4;

    end;

    theorem :: LIMFUNC3:41

    

     Th41: f1 is_convergent_in x0 & f2 is_convergent_in x0 & ( lim (f1,x0)) = ( lim (f2,x0)) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f)) & (ex r st 0 < r & (for g st g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f1 . g) <= (f . g) & (f . g) <= (f2 . g)) & (((( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) c= (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) & (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) c= (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[))) or ((( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) c= (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) & (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) c= (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[))))) implies f is_convergent_in x0 & ( lim (f,x0)) = ( lim (f1,x0))

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_convergent_in x0 and

       A3: ( lim (f1,x0)) = ( lim (f2,x0)) and

       A4: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f);

      given r1 such that

       A5: 0 < r1 and

       A6: for g st g in (( dom f) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) holds (f1 . g) <= (f . g) & (f . g) <= (f2 . g) and

       A7: (( dom f1) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) c= (( dom f2) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) & (( dom f) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) c= (( dom f1) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) or (( dom f2) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) c= (( dom f1) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) & (( dom f) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) c= (( dom f2) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[));

      now

        per cases by A7;

          suppose

           A8: (( dom f1) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) c= (( dom f2) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) & (( dom f) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) c= (( dom f1) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[));

           A9:

          now

            let s be Real_Sequence;

            assume that

             A10: s is convergent and

             A11: ( lim s) = x0 and

             A12: ( rng s) c= (( dom f) \ {x0});

            consider k such that

             A13: for n st k <= n holds (x0 - r1) < (s . n) & (s . n) < (x0 + r1) by A5, A10, A11, Th7;

            

             A14: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

            then

             A15: ( rng (s ^\ k)) c= (( dom f) \ {x0}) by A12;

            now

              let x be object;

              assume

               A16: x in ( rng (s ^\ k));

              then

              consider n such that

               A17: x = ((s ^\ k) . n) by FUNCT_2: 113;

              

               A18: k <= (n + k) by NAT_1: 12;

              then (s . (n + k)) < (x0 + r1) by A13;

              then

               A19: ((s ^\ k) . n) < (x0 + r1) by NAT_1:def 3;

              (x0 - r1) < (s . (n + k)) by A13, A18;

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

              then ((s ^\ k) . n) in { g1 : (x0 - r1) < g1 & g1 < (x0 + r1) } by A19;

              then

               A20: ((s ^\ k) . n) in ].(x0 - r1), (x0 + r1).[ by RCOMP_1:def 2;

               not ((s ^\ k) . n) in {x0} by A15, A16, A17, XBOOLE_0:def 5;

              then x in ( ].(x0 - r1), (x0 + r1).[ \ {x0}) by A17, A20, XBOOLE_0:def 5;

              hence x in ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[) by A5, Th4;

            end;

            then

             A21: ( rng (s ^\ k)) c= ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[);

            

             A22: ( rng s) c= ( dom f) by A12, XBOOLE_1: 1;

            then ( rng (s ^\ k)) c= ( dom f) by A14;

            then

             A23: ( rng (s ^\ k)) c= (( dom f) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) by A21, XBOOLE_1: 19;

            then

             A24: ( rng (s ^\ k)) c= (( dom f1) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) by A8;

            then

             A25: ( rng (s ^\ k)) c= (( dom f2) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) by A8;

            

             A26: ( lim (s ^\ k)) = x0 by A10, A11, SEQ_4: 20;

            

             A27: (( dom f2) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) c= ( dom f2) by XBOOLE_1: 17;

            then

             A28: ( rng (s ^\ k)) c= ( dom f2) by A25;

            

             A29: ( rng (s ^\ k)) c= (( dom f2) \ {x0})

            proof

              let x be object;

              assume

               A30: x in ( rng (s ^\ k));

              then not x in {x0} by A15, XBOOLE_0:def 5;

              hence thesis by A28, A30, XBOOLE_0:def 5;

            end;

            then

             A31: ( lim (f2 /* (s ^\ k))) = ( lim (f2,x0)) by A2, A10, A26, Def4;

            

             A32: (( dom f1) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) c= ( dom f1) by XBOOLE_1: 17;

            then

             A33: ( rng (s ^\ k)) c= ( dom f1) by A24;

            

             A34: ( rng (s ^\ k)) c= (( dom f1) \ {x0})

            proof

              let x be object;

              assume

               A35: x in ( rng (s ^\ k));

              then not x in {x0} by A15, XBOOLE_0:def 5;

              hence thesis by A33, A35, XBOOLE_0:def 5;

            end;

            then

             A36: ( lim (f1 /* (s ^\ k))) = ( lim (f1,x0)) by A1, A10, A26, Def4;

             A37:

            now

              let n be Nat;

              

               A38: n in NAT by ORDINAL1:def 12;

              

               A39: ((s ^\ k) . n) in ( rng (s ^\ k)) by VALUED_0: 28;

              then (f . ((s ^\ k) . n)) <= (f2 . ((s ^\ k) . n)) by A6, A23;

              then

               A40: ((f /* (s ^\ k)) . n) <= (f2 . ((s ^\ k) . n)) by A14, A22, FUNCT_2: 108, XBOOLE_1: 1, A38;

              (f1 . ((s ^\ k) . n)) <= (f . ((s ^\ k) . n)) by A6, A23, A39;

              then (f1 . ((s ^\ k) . n)) <= ((f /* (s ^\ k)) . n) by A14, A22, FUNCT_2: 108, XBOOLE_1: 1, A38;

              hence ((f1 /* (s ^\ k)) . n) <= ((f /* (s ^\ k)) . n) & ((f /* (s ^\ k)) . n) <= ((f2 /* (s ^\ k)) . n) by A32, A27, A24, A25, A40, FUNCT_2: 108, XBOOLE_1: 1, A38;

            end;

            

             A41: (f2 /* (s ^\ k)) is convergent by A2, A10, A26, A29;

            

             A42: (f1 /* (s ^\ k)) is convergent by A1, A10, A26, A34;

            then (f /* (s ^\ k)) is convergent by A3, A36, A41, A31, A37, SEQ_2: 19;

            then

             A43: ((f /* s) ^\ k) is convergent by A12, VALUED_0: 27, XBOOLE_1: 1;

            hence (f /* s) is convergent by SEQ_4: 21;

            ( lim (f /* (s ^\ k))) = ( lim (f1,x0)) by A3, A42, A36, A41, A31, A37, SEQ_2: 20;

            then ( lim ((f /* s) ^\ k)) = ( lim (f1,x0)) by A12, VALUED_0: 27, XBOOLE_1: 1;

            hence ( lim (f /* s)) = ( lim (f1,x0)) by A43, SEQ_4: 22;

          end;

          hence f is_convergent_in x0 by A4;

          hence thesis by A9, Def4;

        end;

          suppose

           A44: (( dom f2) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) c= (( dom f1) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) & (( dom f) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) c= (( dom f2) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[));

           A45:

          now

            let s be Real_Sequence;

            assume that

             A46: s is convergent and

             A47: ( lim s) = x0 and

             A48: ( rng s) c= (( dom f) \ {x0});

            consider k such that

             A49: for n st k <= n holds (x0 - r1) < (s . n) & (s . n) < (x0 + r1) by A5, A46, A47, Th7;

            

             A50: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

            then

             A51: ( rng (s ^\ k)) c= (( dom f) \ {x0}) by A48;

            now

              let x be object;

              assume

               A52: x in ( rng (s ^\ k));

              then

              consider n such that

               A53: x = ((s ^\ k) . n) by FUNCT_2: 113;

              

               A54: k <= (n + k) by NAT_1: 12;

              then (s . (n + k)) < (x0 + r1) by A49;

              then

               A55: ((s ^\ k) . n) < (x0 + r1) by NAT_1:def 3;

              (x0 - r1) < (s . (n + k)) by A49, A54;

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

              then ((s ^\ k) . n) in { g1 : (x0 - r1) < g1 & g1 < (x0 + r1) } by A55;

              then

               A56: ((s ^\ k) . n) in ].(x0 - r1), (x0 + r1).[ by RCOMP_1:def 2;

               not ((s ^\ k) . n) in {x0} by A51, A52, A53, XBOOLE_0:def 5;

              then x in ( ].(x0 - r1), (x0 + r1).[ \ {x0}) by A53, A56, XBOOLE_0:def 5;

              hence x in ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[) by A5, Th4;

            end;

            then

             A57: ( rng (s ^\ k)) c= ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[);

            

             A58: ( rng s) c= ( dom f) by A48, XBOOLE_1: 1;

            then ( rng (s ^\ k)) c= ( dom f) by A50;

            then

             A59: ( rng (s ^\ k)) c= (( dom f) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) by A57, XBOOLE_1: 19;

            then

             A60: ( rng (s ^\ k)) c= (( dom f2) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) by A44;

            then

             A61: ( rng (s ^\ k)) c= (( dom f1) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) by A44;

            

             A62: ( lim (s ^\ k)) = x0 by A46, A47, SEQ_4: 20;

            

             A63: (( dom f2) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) c= ( dom f2) by XBOOLE_1: 17;

            then

             A64: ( rng (s ^\ k)) c= ( dom f2) by A60;

            

             A65: ( rng (s ^\ k)) c= (( dom f2) \ {x0})

            proof

              let x be object;

              assume

               A66: x in ( rng (s ^\ k));

              then not x in {x0} by A51, XBOOLE_0:def 5;

              hence thesis by A64, A66, XBOOLE_0:def 5;

            end;

            then

             A67: ( lim (f2 /* (s ^\ k))) = ( lim (f2,x0)) by A2, A46, A62, Def4;

            

             A68: (( dom f1) /\ ( ].(x0 - r1), x0.[ \/ ].x0, (x0 + r1).[)) c= ( dom f1) by XBOOLE_1: 17;

            then

             A69: ( rng (s ^\ k)) c= ( dom f1) by A61;

            

             A70: ( rng (s ^\ k)) c= (( dom f1) \ {x0})

            proof

              let x be object;

              assume

               A71: x in ( rng (s ^\ k));

              then not x in {x0} by A51, XBOOLE_0:def 5;

              hence thesis by A69, A71, XBOOLE_0:def 5;

            end;

            then

             A72: ( lim (f1 /* (s ^\ k))) = ( lim (f1,x0)) by A1, A46, A62, Def4;

             A73:

            now

              let n be Nat;

              

               A74: n in NAT by ORDINAL1:def 12;

              

               A75: ((s ^\ k) . n) in ( rng (s ^\ k)) by VALUED_0: 28;

              then (f . ((s ^\ k) . n)) <= (f2 . ((s ^\ k) . n)) by A6, A59;

              then

               A76: ((f /* (s ^\ k)) . n) <= (f2 . ((s ^\ k) . n)) by A50, A58, FUNCT_2: 108, XBOOLE_1: 1, A74;

              (f1 . ((s ^\ k) . n)) <= (f . ((s ^\ k) . n)) by A6, A59, A75;

              then (f1 . ((s ^\ k) . n)) <= ((f /* (s ^\ k)) . n) by A50, A58, FUNCT_2: 108, XBOOLE_1: 1, A74;

              hence ((f1 /* (s ^\ k)) . n) <= ((f /* (s ^\ k)) . n) & ((f /* (s ^\ k)) . n) <= ((f2 /* (s ^\ k)) . n) by A68, A63, A60, A61, A76, FUNCT_2: 108, XBOOLE_1: 1, A74;

            end;

            

             A77: (f2 /* (s ^\ k)) is convergent by A2, A46, A62, A65;

            

             A78: (f1 /* (s ^\ k)) is convergent by A1, A46, A62, A70;

            then (f /* (s ^\ k)) is convergent by A3, A72, A77, A67, A73, SEQ_2: 19;

            then

             A79: ((f /* s) ^\ k) is convergent by A48, VALUED_0: 27, XBOOLE_1: 1;

            hence (f /* s) is convergent by SEQ_4: 21;

            ( lim (f /* (s ^\ k))) = ( lim (f1,x0)) by A3, A78, A72, A77, A67, A73, SEQ_2: 20;

            then ( lim ((f /* s) ^\ k)) = ( lim (f1,x0)) by A48, VALUED_0: 27, XBOOLE_1: 1;

            hence ( lim (f /* s)) = ( lim (f1,x0)) by A79, SEQ_4: 22;

          end;

          hence f is_convergent_in x0 by A4;

          hence thesis by A45, Def4;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC3:42

    f1 is_convergent_in x0 & f2 is_convergent_in x0 & ( lim (f1,x0)) = ( lim (f2,x0)) & (ex r st 0 < r & ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) c= ((( dom f1) /\ ( dom f2)) /\ ( dom f)) & for g st g in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) holds (f1 . g) <= (f . g) & (f . g) <= (f2 . g)) implies f is_convergent_in x0 & ( lim (f,x0)) = ( lim (f1,x0))

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_convergent_in x0 and

       A3: ( lim (f1,x0)) = ( lim (f2,x0));

      given r such that

       A4: 0 < r and

       A5: ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) c= ((( dom f1) /\ ( dom f2)) /\ ( dom f)) and

       A6: for g st g in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) holds (f1 . g) <= (f . g) & (f . g) <= (f2 . g);

      

       A7: (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) = ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by A5, XBOOLE_1: 18, XBOOLE_1: 28;

      

       A8: ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) c= (( dom f1) /\ ( dom f2)) by A5, XBOOLE_1: 18;

      then

       A9: (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) = ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by XBOOLE_1: 18, XBOOLE_1: 28;

      

       A10: (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) = ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by A8, XBOOLE_1: 18, XBOOLE_1: 28;

      for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) by A4, A5, Th5, XBOOLE_1: 18;

      hence thesis by A1, A2, A3, A4, A6, A7, A9, A10, Th41;

    end;

    theorem :: LIMFUNC3:43

    f1 is_convergent_in x0 & f2 is_convergent_in x0 & (ex r st 0 < r & (((( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) c= (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) & for g st g in (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f1 . g) <= (f2 . g)) or ((( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) c= (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) & for g st g in (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f1 . g) <= (f2 . g)))) implies ( lim (f1,x0)) <= ( lim (f2,x0))

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_convergent_in x0;

      given r such that

       A3: 0 < r and

       A4: ((( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) c= (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) & for g st g in (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f1 . g) <= (f2 . g)) or ((( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) c= (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) & for g st g in (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f1 . g) <= (f2 . g));

      now

        per cases by A4;

          suppose

           A5: (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) c= (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) & for g st g in (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f1 . g) <= (f2 . g);

          defpred X[ Nat, Real] means (x0 - (1 / ($1 + 1))) < $2 & $2 < x0 & $2 in ( dom f1);

           A6:

          now

            let n be Element of NAT ;

            

             A7: x0 < (x0 + 1) by Lm1;

            (x0 - (1 / (n + 1))) < x0 by Lm3;

            then

            consider g1, g2 such that

             A8: (x0 - (1 / (n + 1))) < g1 and

             A9: g1 < x0 and

             A10: g1 in ( dom f1) and g2 < (x0 + 1) and x0 < g2 and g2 in ( dom f1) by A1, A7;

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

            take g1;

            thus X[n, g1] by A8, A9, A10;

          end;

          consider s be Real_Sequence such that

           A11: for n holds X[n, (s . n)] from FUNCT_2:sch 3( A6);

          

           A12: ( lim s) = x0 by A11, Th6;

          

           A13: ( rng s) c= (( dom f1) \ {x0}) by A11, Th6;

          

           A14: s is convergent by A11, Th6;

          (x0 - r) < x0 by A3, Lm1;

          then

          consider k be Nat such that

           A15: for n be Nat st k <= n holds (x0 - r) < (s . n) by A14, A12, LIMFUNC2: 1;

          

           A16: ( lim (s ^\ k)) = x0 by A14, A12, SEQ_4: 20;

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

          then

           A17: ( rng (s ^\ k)) c= (( dom f1) \ {x0}) by A13;

          then

           A18: ( lim (f1 /* (s ^\ k))) = ( lim (f1,x0)) by A1, A14, A16, Def4;

          now

            let x be object;

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

            then

            consider n such that

             A19: ((s ^\ k) . n) = x by FUNCT_2: 113;

            

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

            (s . (n + k)) < x0 by A11, A20;

            then

             A21: ((s ^\ k) . n) < x0 by NAT_1:def 3;

            (x0 - r) < (s . (n + k)) by A15, NAT_1: 12;

            then (x0 - r) < ((s ^\ k) . n) by NAT_1:def 3;

            then ((s ^\ k) . n) in { g2 : (x0 - r) < g2 & g2 < x0 } by A21;

            then ((s ^\ k) . n) in ].(x0 - r), x0.[ by RCOMP_1:def 2;

            then

             A22: ((s ^\ k) . n) in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by XBOOLE_0:def 3;

            (s . (n + k)) in ( dom f1) by A11, A20;

            then ((s ^\ k) . n) in ( dom f1) by NAT_1:def 3;

            hence x in (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A19, A22, XBOOLE_0:def 4;

          end;

          then

           A23: ( rng (s ^\ k)) c= (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[));

          then

           A24: ( rng (s ^\ k)) c= (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A5;

           A25:

          now

            let n be Nat;

            

             A26: n in NAT by ORDINAL1:def 12;

            ((s ^\ k) . n) in ( rng (s ^\ k)) by VALUED_0: 28;

            then (f1 . ((s ^\ k) . n)) <= (f2 . ((s ^\ k) . n)) by A5, A23;

            then (f1 . ((s ^\ k) . n)) <= ((f2 /* (s ^\ k)) . n) by A24, FUNCT_2: 108, XBOOLE_1: 18, A26;

            hence ((f1 /* (s ^\ k)) . n) <= ((f2 /* (s ^\ k)) . n) by A23, FUNCT_2: 108, XBOOLE_1: 18, A26;

          end;

          

           A27: ( rng (s ^\ k)) c= ( dom f2) by A24, XBOOLE_1: 18;

          

           A28: ( rng (s ^\ k)) c= (( dom f2) \ {x0})

          proof

            let x be object;

            assume

             A29: x in ( rng (s ^\ k));

            then not x in {x0} by A17, XBOOLE_0:def 5;

            hence thesis by A27, A29, XBOOLE_0:def 5;

          end;

          then

           A30: ( lim (f2 /* (s ^\ k))) = ( lim (f2,x0)) by A2, A14, A16, Def4;

          

           A31: (f2 /* (s ^\ k)) is convergent by A2, A14, A16, A28;

          (f1 /* (s ^\ k)) is convergent by A1, A14, A16, A17;

          hence thesis by A18, A31, A30, A25, SEQ_2: 18;

        end;

          suppose

           A32: (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) c= (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) & for g st g in (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f1 . g) <= (f2 . g);

          defpred X[ Element of NAT , Real] means (x0 - (1 / ($1 + 1))) < $2 & $2 < x0 & $2 in ( dom f2);

           A33:

          now

            let n;

            

             A34: x0 < (x0 + 1) by Lm1;

            (x0 - (1 / (n + 1))) < x0 by Lm3;

            then

            consider g1, g2 such that

             A35: (x0 - (1 / (n + 1))) < g1 and

             A36: g1 < x0 and

             A37: g1 in ( dom f2) and g2 < (x0 + 1) and x0 < g2 and g2 in ( dom f2) by A2, A34;

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

            take g1;

            thus X[n, g1] by A35, A36, A37;

          end;

          consider s be Real_Sequence such that

           A38: for n holds X[n, (s . n)] from FUNCT_2:sch 3( A33);

          

           A39: ( lim s) = x0 by A38, Th6;

          

           A40: ( rng s) c= (( dom f2) \ {x0}) by A38, Th6;

          

           A41: s is convergent by A38, Th6;

          (x0 - r) < x0 by A3, Lm1;

          then

          consider k be Nat such that

           A42: for n be Nat st k <= n holds (x0 - r) < (s . n) by A41, A39, LIMFUNC2: 1;

          

           A43: ( lim (s ^\ k)) = x0 by A41, A39, SEQ_4: 20;

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

          then

           A44: ( rng (s ^\ k)) c= (( dom f2) \ {x0}) by A40;

          then

           A45: ( lim (f2 /* (s ^\ k))) = ( lim (f2,x0)) by A2, A41, A43, Def4;

           A46:

          now

            let x be object;

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

            then

            consider n such that

             A47: ((s ^\ k) . n) = x by FUNCT_2: 113;

            

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

            (s . (n + k)) < x0 by A38, A48;

            then

             A49: ((s ^\ k) . n) < x0 by NAT_1:def 3;

            (x0 - r) < (s . (n + k)) by A42, NAT_1: 12;

            then (x0 - r) < ((s ^\ k) . n) by NAT_1:def 3;

            then ((s ^\ k) . n) in { g2 : (x0 - r) < g2 & g2 < x0 } by A49;

            then ((s ^\ k) . n) in ].(x0 - r), x0.[ by RCOMP_1:def 2;

            then

             A50: ((s ^\ k) . n) in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by XBOOLE_0:def 3;

            (s . (n + k)) in ( dom f2) by A38, A48;

            then ((s ^\ k) . n) in ( dom f2) by NAT_1:def 3;

            hence x in (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A47, A50, XBOOLE_0:def 4;

          end;

          then

           A51: ( rng (s ^\ k)) c= (( dom f2) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[));

          then

           A52: ( rng (s ^\ k)) c= (( dom f1) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A32;

           A53:

          now

            let n be Nat;

            

             A54: n in NAT by ORDINAL1:def 12;

            ((s ^\ k) . n) in ( rng (s ^\ k)) by VALUED_0: 28;

            then (f1 . ((s ^\ k) . n)) <= (f2 . ((s ^\ k) . n)) by A32, A46;

            then (f1 . ((s ^\ k) . n)) <= ((f2 /* (s ^\ k)) . n) by A51, FUNCT_2: 108, XBOOLE_1: 18, A54;

            hence ((f1 /* (s ^\ k)) . n) <= ((f2 /* (s ^\ k)) . n) by A52, FUNCT_2: 108, XBOOLE_1: 18, A54;

          end;

          

           A55: ( rng (s ^\ k)) c= ( dom f1) by A52, XBOOLE_1: 18;

          

           A56: ( rng (s ^\ k)) c= (( dom f1) \ {x0})

          proof

            let x be object;

            assume

             A57: x in ( rng (s ^\ k));

            then not x in {x0} by A44, XBOOLE_0:def 5;

            hence thesis by A55, A57, XBOOLE_0:def 5;

          end;

          then

           A58: ( lim (f1 /* (s ^\ k))) = ( lim (f1,x0)) by A1, A41, A43, Def4;

          

           A59: (f1 /* (s ^\ k)) is convergent by A1, A41, A43, A56;

          (f2 /* (s ^\ k)) is convergent by A2, A41, A43, A44;

          hence thesis by A45, A59, A58, A53, SEQ_2: 18;

        end;

      end;

      hence thesis;

    end;

    theorem :: LIMFUNC3:44

    (f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) & (f . g1) <> 0 & (f . g2) <> 0 ) implies (f ^ ) is_convergent_in x0 & ( lim ((f ^ ),x0)) = 0

    proof

      

       A1: (( dom f) \ (f " { 0 })) = ( dom (f ^ )) by RFUNCT_1:def 2;

      assume

       A2: f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0;

       A3:

      now

        let seq;

        assume that

         A4: seq is convergent and

         A5: ( lim seq) = x0 and

         A6: ( rng seq) c= (( dom (f ^ )) \ {x0});

        ( rng seq) c= ( dom (f ^ )) by A6, XBOOLE_1: 1;

        then

         A7: ( rng seq) c= ( dom f) by A1, XBOOLE_1: 1;

        

         A8: ( rng seq) c= (( dom f) \ {x0})

        proof

          let x be object;

          assume

           A9: x in ( rng seq);

          then not x in {x0} by A6, XBOOLE_0:def 5;

          hence thesis by A7, A9, XBOOLE_0:def 5;

        end;

        now

          per cases by A2;

            suppose f is_divergent_to+infty_in x0;

            then

             A10: (f /* seq) is divergent_to+infty by A4, A5, A8;

            then

             A11: ( lim ((f /* seq) " )) = 0 by LIMFUNC1: 34;

            ((f /* seq) " ) is convergent by A10, LIMFUNC1: 34;

            hence ((f ^ ) /* seq) is convergent & ( lim ((f ^ ) /* seq)) = 0 by A6, A11, RFUNCT_2: 12, XBOOLE_1: 1;

          end;

            suppose f is_divergent_to-infty_in x0;

            then

             A12: (f /* seq) is divergent_to-infty by A4, A5, A8;

            then

             A13: ( lim ((f /* seq) " )) = 0 by LIMFUNC1: 34;

            ((f /* seq) " ) is convergent by A12, LIMFUNC1: 34;

            hence ((f ^ ) /* seq) is convergent & ( lim ((f ^ ) /* seq)) = 0 by A6, A13, RFUNCT_2: 12, XBOOLE_1: 1;

          end;

        end;

        hence ((f ^ ) /* seq) is convergent & ( lim ((f ^ ) /* seq)) = 0 ;

      end;

      assume

       A14: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) & (f . g1) <> 0 & (f . g2) <> 0 ;

      now

        let r1, r2;

        assume that

         A15: r1 < x0 and

         A16: x0 < r2;

        consider g1, g2 such that

         A17: r1 < g1 and

         A18: g1 < x0 and

         A19: g1 in ( dom f) and

         A20: g2 < r2 and

         A21: x0 < g2 and

         A22: g2 in ( dom f) and

         A23: (f . g1) <> 0 and

         A24: (f . g2) <> 0 by A14, A15, A16;

        take g1, g2;

         not (f . g2) in { 0 } by A24, TARSKI:def 1;

        then

         A25: not g2 in (f " { 0 }) by FUNCT_1:def 7;

         not (f . g1) in { 0 } by A23, TARSKI:def 1;

        then not g1 in (f " { 0 }) by FUNCT_1:def 7;

        hence r1 < g1 & g1 < x0 & g1 in ( dom (f ^ )) & g2 < r2 & x0 < g2 & g2 in ( dom (f ^ )) by A1, A17, A18, A19, A20, A21, A22, A25, XBOOLE_0:def 5;

      end;

      hence (f ^ ) is_convergent_in x0 by A3;

      hence thesis by A3, Def4;

    end;

    theorem :: LIMFUNC3:45

    f is_convergent_in x0 & ( lim (f,x0)) = 0 & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) & (f . g1) <> 0 & (f . g2) <> 0 ) & (ex r st 0 < r & for g st g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds 0 <= (f . g)) implies (f ^ ) is_divergent_to+infty_in x0

    proof

      assume that

       A1: f is_convergent_in x0 and

       A2: ( lim (f,x0)) = 0 and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) & (f . g1) <> 0 & (f . g2) <> 0 ;

      given r such that

       A4: 0 < r and

       A5: for g st g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds 0 <= (f . g);

      thus for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f ^ )) & g2 < r2 & x0 < g2 & g2 in ( dom (f ^ ))

      proof

        let r1, r2;

        assume that

         A6: r1 < x0 and

         A7: x0 < r2;

        consider g1, g2 such that

         A8: r1 < g1 and

         A9: g1 < x0 and

         A10: g1 in ( dom f) and

         A11: g2 < r2 and

         A12: x0 < g2 and

         A13: g2 in ( dom f) and

         A14: (f . g1) <> 0 and

         A15: (f . g2) <> 0 by A3, A6, A7;

         not (f . g2) in { 0 } by A15, TARSKI:def 1;

        then not g2 in (f " { 0 }) by FUNCT_1:def 7;

        then

         A16: g2 in (( dom f) \ (f " { 0 })) by A13, XBOOLE_0:def 5;

        take g1, g2;

         not (f . g1) in { 0 } by A14, TARSKI:def 1;

        then not g1 in (f " { 0 }) by FUNCT_1:def 7;

        then g1 in (( dom f) \ (f " { 0 })) by A10, XBOOLE_0:def 5;

        hence thesis by A8, A9, A11, A12, A16, RFUNCT_1:def 2;

      end;

      let s be Real_Sequence;

      assume that

       A17: s is convergent and

       A18: ( lim s) = x0 and

       A19: ( rng s) c= (( dom (f ^ )) \ {x0});

      consider k such that

       A20: for n st k <= n holds (x0 - r) < (s . n) & (s . n) < (x0 + r) by A4, A17, A18, Th7;

      

       A21: ( rng s) c= ( dom (f ^ )) by A19, XBOOLE_1: 1;

      

       A22: ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

      

      then

       A23: ((f /* (s ^\ k)) " ) = (((f /* s) ^\ k) " ) by A21, VALUED_0: 27, XBOOLE_1: 1

      .= (((f /* s) " ) ^\ k) by SEQM_3: 18

      .= (((f ^ ) /* s) ^\ k) by A19, RFUNCT_2: 12, XBOOLE_1: 1;

      

       A24: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

      

       A25: ( rng s) c= ( dom f) by A21, A22, XBOOLE_1: 1;

      then

       A26: ( rng (s ^\ k)) c= ( dom f) by A24;

      

       A27: ( rng (s ^\ k)) c= (( dom (f ^ )) \ {x0}) by A19, A24;

      

       A28: ( rng (s ^\ k)) c= (( dom f) \ {x0})

      proof

        let x be object;

        assume

         A29: x in ( rng (s ^\ k));

        then not x in {x0} by A27, XBOOLE_0:def 5;

        hence thesis by A26, A29, XBOOLE_0:def 5;

      end;

      

       A30: ( lim (s ^\ k)) = x0 by A17, A18, SEQ_4: 20;

      then

       A31: ( lim (f /* (s ^\ k))) = 0 by A1, A2, A17, A28, Def4;

      

       A32: (f /* (s ^\ k)) is non-zero by A21, A24, RFUNCT_2: 11, XBOOLE_1: 1;

      now

        let n be Nat;

        

         A33: n in NAT by ORDINAL1:def 12;

        

         A34: k <= (n + k) by NAT_1: 12;

        then (s . (n + k)) < (x0 + r) by A20;

        then

         A35: ((s ^\ k) . n) < (x0 + r) by NAT_1:def 3;

        (x0 - r) < (s . (n + k)) by A20, A34;

        then (x0 - r) < ((s ^\ k) . n) by NAT_1:def 3;

        then ((s ^\ k) . n) in { g1 : (x0 - r) < g1 & g1 < (x0 + r) } by A35;

        then

         A36: ((s ^\ k) . n) in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        

         A37: ((s ^\ k) . n) in ( rng (s ^\ k)) by VALUED_0: 28;

        then not ((s ^\ k) . n) in {x0} by A27, XBOOLE_0:def 5;

        then ((s ^\ k) . n) in ( ].(x0 - r), (x0 + r).[ \ {x0}) by A36, XBOOLE_0:def 5;

        then ((s ^\ k) . n) in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by A4, Th4;

        then ((s ^\ k) . n) in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A26, A37, XBOOLE_0:def 4;

        then

         A38: 0 <= (f . ((s ^\ k) . n)) by A5;

        ((f /* (s ^\ k)) . n) <> 0 by A32, SEQ_1: 5;

        hence 0 < ((f /* (s ^\ k)) . n) by A25, A24, A38, FUNCT_2: 108, XBOOLE_1: 1, A33;

      end;

      then

       A39: for n be Nat holds 0 <= n implies 0 < ((f /* (s ^\ k)) . n);

      (f /* (s ^\ k)) is convergent by A1, A17, A30, A28;

      then ((f /* (s ^\ k)) " ) is divergent_to+infty by A31, A39, LIMFUNC1: 35;

      hence thesis by A23, LIMFUNC1: 7;

    end;

    theorem :: LIMFUNC3:46

    f is_convergent_in x0 & ( lim (f,x0)) = 0 & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) & (f . g1) <> 0 & (f . g2) <> 0 ) & (ex r st 0 < r & for g st g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f . g) <= 0 ) implies (f ^ ) is_divergent_to-infty_in x0

    proof

      assume that

       A1: f is_convergent_in x0 and

       A2: ( lim (f,x0)) = 0 and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom f) & g2 < r2 & x0 < g2 & g2 in ( dom f) & (f . g1) <> 0 & (f . g2) <> 0 ;

      given r such that

       A4: 0 < r and

       A5: for g st g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f . g) <= 0 ;

      thus for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f ^ )) & g2 < r2 & x0 < g2 & g2 in ( dom (f ^ ))

      proof

        let r1, r2;

        assume that

         A6: r1 < x0 and

         A7: x0 < r2;

        consider g1, g2 such that

         A8: r1 < g1 and

         A9: g1 < x0 and

         A10: g1 in ( dom f) and

         A11: g2 < r2 and

         A12: x0 < g2 and

         A13: g2 in ( dom f) and

         A14: (f . g1) <> 0 and

         A15: (f . g2) <> 0 by A3, A6, A7;

         not (f . g2) in { 0 } by A15, TARSKI:def 1;

        then not g2 in (f " { 0 }) by FUNCT_1:def 7;

        then

         A16: g2 in (( dom f) \ (f " { 0 })) by A13, XBOOLE_0:def 5;

        take g1, g2;

         not (f . g1) in { 0 } by A14, TARSKI:def 1;

        then not g1 in (f " { 0 }) by FUNCT_1:def 7;

        then g1 in (( dom f) \ (f " { 0 })) by A10, XBOOLE_0:def 5;

        hence thesis by A8, A9, A11, A12, A16, RFUNCT_1:def 2;

      end;

      let s be Real_Sequence;

      assume that

       A17: s is convergent and

       A18: ( lim s) = x0 and

       A19: ( rng s) c= (( dom (f ^ )) \ {x0});

      consider k such that

       A20: for n st k <= n holds (x0 - r) < (s . n) & (s . n) < (x0 + r) by A4, A17, A18, Th7;

      

       A21: ( rng s) c= ( dom (f ^ )) by A19, XBOOLE_1: 1;

      

       A22: ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

      

      then

       A23: ((f /* (s ^\ k)) " ) = (((f /* s) ^\ k) " ) by A21, VALUED_0: 27, XBOOLE_1: 1

      .= (((f /* s) " ) ^\ k) by SEQM_3: 18

      .= (((f ^ ) /* s) ^\ k) by A19, RFUNCT_2: 12, XBOOLE_1: 1;

      

       A24: ( rng (s ^\ k)) c= ( rng s) by VALUED_0: 21;

      

       A25: ( rng s) c= ( dom f) by A21, A22, XBOOLE_1: 1;

      then

       A26: ( rng (s ^\ k)) c= ( dom f) by A24;

      

       A27: ( rng (s ^\ k)) c= (( dom (f ^ )) \ {x0}) by A19, A24;

      

       A28: ( rng (s ^\ k)) c= (( dom f) \ {x0})

      proof

        let x be object;

        assume

         A29: x in ( rng (s ^\ k));

        then not x in {x0} by A27, XBOOLE_0:def 5;

        hence thesis by A26, A29, XBOOLE_0:def 5;

      end;

      

       A30: ( lim (s ^\ k)) = x0 by A17, A18, SEQ_4: 20;

      then

       A31: ( lim (f /* (s ^\ k))) = 0 by A1, A2, A17, A28, Def4;

      

       A32: (f /* (s ^\ k)) is non-zero by A21, A24, RFUNCT_2: 11, XBOOLE_1: 1;

       A33:

      now

        let n;

        

         A34: k <= (n + k) by NAT_1: 12;

        then (s . (n + k)) < (x0 + r) by A20;

        then

         A35: ((s ^\ k) . n) < (x0 + r) by NAT_1:def 3;

        (x0 - r) < (s . (n + k)) by A20, A34;

        then (x0 - r) < ((s ^\ k) . n) by NAT_1:def 3;

        then ((s ^\ k) . n) in { g1 : (x0 - r) < g1 & g1 < (x0 + r) } by A35;

        then

         A36: ((s ^\ k) . n) in ].(x0 - r), (x0 + r).[ by RCOMP_1:def 2;

        

         A37: ((s ^\ k) . n) in ( rng (s ^\ k)) by VALUED_0: 28;

        then not ((s ^\ k) . n) in {x0} by A27, XBOOLE_0:def 5;

        then ((s ^\ k) . n) in ( ].(x0 - r), (x0 + r).[ \ {x0}) by A36, XBOOLE_0:def 5;

        then ((s ^\ k) . n) in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by A4, Th4;

        then ((s ^\ k) . n) in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A26, A37, XBOOLE_0:def 4;

        then

         A38: (f . ((s ^\ k) . n)) <= 0 by A5;

        ((f /* (s ^\ k)) . n) <> 0 by A32, SEQ_1: 5;

        hence ((f /* (s ^\ k)) . n) < 0 by A25, A24, A38, FUNCT_2: 108, XBOOLE_1: 1;

      end;

      

       A39: for n be Nat holds 0 <= n implies ((f /* (s ^\ k)) . n) < 0

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A33;

      end;

      (f /* (s ^\ k)) is convergent by A1, A17, A30, A28;

      then ((f /* (s ^\ k)) " ) is divergent_to-infty by A31, A39, LIMFUNC1: 36;

      hence thesis by A23, LIMFUNC1: 7;

    end;

    theorem :: LIMFUNC3:47

    f is_convergent_in x0 & ( lim (f,x0)) = 0 & (ex r st 0 < r & for g st g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds 0 < (f . g)) implies (f ^ ) is_divergent_to+infty_in x0

    proof

      assume that

       A1: f is_convergent_in x0 and

       A2: ( lim (f,x0)) = 0 ;

      

       A3: f is_right_convergent_in x0 by A1, Th29;

      given r such that

       A4: 0 < r and

       A5: for g st g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds 0 < (f . g);

       A6:

      now

        let g;

        assume

         A7: g in (( dom f) /\ ].x0, (x0 + r).[);

        then g in ].x0, (x0 + r).[ by XBOOLE_0:def 4;

        then

         A8: g in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by XBOOLE_0:def 3;

        g in ( dom f) by A7, XBOOLE_0:def 4;

        then g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A8, XBOOLE_0:def 4;

        hence 0 < (f . g) by A5;

      end;

       A9:

      now

        let g;

        assume

         A10: g in (( dom f) /\ ].(x0 - r), x0.[);

        then g in ].(x0 - r), x0.[ by XBOOLE_0:def 4;

        then

         A11: g in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by XBOOLE_0:def 3;

        g in ( dom f) by A10, XBOOLE_0:def 4;

        then g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A11, XBOOLE_0:def 4;

        hence 0 < (f . g) by A5;

      end;

      ( lim_right (f,x0)) = 0 by A1, A2, Th29;

      then

       A12: (f ^ ) is_right_divergent_to+infty_in x0 by A3, A4, A6, LIMFUNC2: 73;

      

       A13: f is_left_convergent_in x0 by A1, Th29;

      ( lim_left (f,x0)) = 0 by A1, A2, Th29;

      then (f ^ ) is_left_divergent_to+infty_in x0 by A13, A4, A9, LIMFUNC2: 71;

      hence thesis by A12, Th12;

    end;

    theorem :: LIMFUNC3:48

    f is_convergent_in x0 & ( lim (f,x0)) = 0 & (ex r st 0 < r & for g st g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f . g) < 0 ) implies (f ^ ) is_divergent_to-infty_in x0

    proof

      assume that

       A1: f is_convergent_in x0 and

       A2: ( lim (f,x0)) = 0 ;

      

       A3: f is_right_convergent_in x0 by A1, Th29;

      given r such that

       A4: 0 < r and

       A5: for g st g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) holds (f . g) < 0 ;

       A6:

      now

        let g;

        assume

         A7: g in (( dom f) /\ ].x0, (x0 + r).[);

        then g in ].x0, (x0 + r).[ by XBOOLE_0:def 4;

        then

         A8: g in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by XBOOLE_0:def 3;

        g in ( dom f) by A7, XBOOLE_0:def 4;

        then g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A8, XBOOLE_0:def 4;

        hence (f . g) < 0 by A5;

      end;

       A9:

      now

        let g;

        assume

         A10: g in (( dom f) /\ ].(x0 - r), x0.[);

        then g in ].(x0 - r), x0.[ by XBOOLE_0:def 4;

        then

         A11: g in ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[) by XBOOLE_0:def 3;

        g in ( dom f) by A10, XBOOLE_0:def 4;

        then g in (( dom f) /\ ( ].(x0 - r), x0.[ \/ ].x0, (x0 + r).[)) by A11, XBOOLE_0:def 4;

        hence (f . g) < 0 by A5;

      end;

      ( lim_right (f,x0)) = 0 by A1, A2, Th29;

      then

       A12: (f ^ ) is_right_divergent_to-infty_in x0 by A3, A4, A6, LIMFUNC2: 74;

      

       A13: f is_left_convergent_in x0 by A1, Th29;

      ( lim_left (f,x0)) = 0 by A1, A2, Th29;

      then (f ^ ) is_left_divergent_to-infty_in x0 by A13, A4, A9, LIMFUNC2: 72;

      hence thesis by A12, Th13;

    end;