LIMFUNC2

:: One-Side Limits of a Real Function at a Point
::  by Jaros{\l}aw Kotowicz
::
:: Received August 20, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, REAL_1, SUBSET_1, SEQ_1, PARTFUN1, CARD_1, ARYTM_3,
      XXREAL_0, ARYTM_1, RELAT_1, TARSKI, VALUED_1, XBOOLE_0, SEQ_2, ORDINAL2,
      FUNCT_1, LIMFUNC1, FUNCT_2, XXREAL_1, COMPLEX1, XXREAL_2, NAT_1,
      VALUED_0, ORDINAL4, LIMFUNC2, ASYMPT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1,
      SEQ_1, COMSEQ_2, SEQ_2, RELSET_1, RCOMP_1, PARTFUN1, RFUNCT_1, LIMFUNC1,
      XXREAL_0;
 constructors FUNCOP_1, REAL_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3, PROB_1,
      RCOMP_1, RFUNCT_1, RFUNCT_2, LIMFUNC1, PARTFUN1, VALUED_1, RELSET_1,
      BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1;
 registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, XBOOLE_0,
      VALUED_0, VALUED_1, FUNCT_2, SEQ_4, SEQ_1, SEQ_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 equalities LIMFUNC1, PROB_1, VALUED_1;
 expansions LIMFUNC1;
 theorems TARSKI, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, SEQ_4, RFUNCT_1,
      RFUNCT_2, LIMFUNC1, RCOMP_1, FUNCT_1, XREAL_0, XBOOLE_0, XBOOLE_1,
      XCMPLX_0, XREAL_1, COMPLEX1, XXREAL_0, VALUED_1, XXREAL_1, FUNCT_2,
      VALUED_0, ORDINAL1;
 schemes SEQ_1, FUNCT_2;

begin

reserve r,r1,r2,g,g1,g2,x0,t for Real;
reserve n,k for Nat;
reserve seq for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL,REAL;

Lm1: for r,g,r1 be Real holds 0<g & r<=r1 implies r-g<r1 & r<r1+g
proof
  let r,g,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 Subset of REAL st rng seq c=dom(f1(#)f2)/\X holds rng seq c=dom(
f1(#)f2) & rng seq c= X & 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 Subset of REAL such that
A1: rng seq c=dom(f1(#)f2)/\X;
A2: dom(f1(#)f2)/\X c=X by XBOOLE_1:17;
  dom(f1(#)f2)/\X c=dom(f1(#)f2) by XBOOLE_1:17;
  hence
A3: rng seq c=dom(f1(#)f2) & rng seq c=X by A1,A2,XBOOLE_1:1;
  thus
A4: dom(f1(#)f2)=dom f1/\dom f2 by VALUED_1:def 4;
  then
A5: dom(f1(#)f2)c=dom f2 by XBOOLE_1:17;
  dom(f1(#)f2)c=dom f1 by A4,XBOOLE_1:17;
  hence rng seq c=dom f1 & rng seq c=dom f2 by A3,A5,XBOOLE_1:1;
  hence thesis by A3,XBOOLE_1:19;
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 Subset of REAL st rng seq c=dom(f1+f2)/\X holds rng seq c=dom(f1
+f2) & rng seq c= X & dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1/\X & rng seq
c=dom f2/\X
proof
  let X be Subset of REAL such that
A1: rng seq c=dom(f1+f2)/\X;
A2: dom(f1+f2)/\X c=X by XBOOLE_1:17;
  dom(f1+f2)/\X c=dom(f1+f2) by XBOOLE_1:17;
  hence
A3: rng seq c=dom(f1+f2) & rng seq c=X by A1,A2,XBOOLE_1:1;
  thus
A4: dom(f1+f2)=dom f1/\dom f2 by VALUED_1:def 1;
  then dom(f1+f2)c=dom f2 by XBOOLE_1:17;
  then
A5: rng seq c=dom f2 by A3,XBOOLE_1:1;
  dom(f1+f2)c=dom f1 by A4,XBOOLE_1:17;
  then rng seq c=dom f1 by A3,XBOOLE_1:1;
  hence thesis by A3,A5,XBOOLE_1:19;
end;

theorem Th1:
  seq is convergent & r<lim seq implies ex n st for k st n<=k holds r<seq.k
proof
  assume that
A1: seq is convergent and
A2: r<lim seq;
  reconsider rr = r as Element of REAL by XREAL_0:def 1;
  set s = seq_const r;
A3: seq-s is convergent by A1;
  s.0=r by SEQ_1:57;
  then lim s=r by SEQ_4:25;
  then lim(seq-s)=lim seq -r by A1,SEQ_2:12;
  then consider n such that
A4: for k st n<= k holds 0<(seq-s).k by A2,A3,LIMFUNC1:4,XREAL_1:50;
  take n;
  let k;
  assume n<=k;
  then 0<(seq-s).k by A4;
  then 0<seq.k-s.k by RFUNCT_2:1;
  then 0<seq.k-r by SEQ_1:57;
  then 0+r<seq .k by XREAL_1:20;
  hence thesis;
end;

theorem Th2:
  seq is convergent & lim seq<r implies ex n st for k st n<=k holds seq.k<r
proof
  assume that
A1: seq is convergent and
A2: lim seq<r;
  reconsider rr = r as Element of REAL by XREAL_0:def 1;
  set s = seq_const r;
A3: s-seq is convergent by A1;
  s.0=r by SEQ_1:57;
  then lim s=r by SEQ_4:25;
  then lim(s-seq)=r-lim seq by A1,SEQ_2:12;
  then consider n such that
A4: for k st n<=k holds 0<(s-seq).k by A2,A3,LIMFUNC1:4,XREAL_1:50;
  take n;
  let k;
  assume n<=k;
  then 0<(s-seq).k by A4;
  then 0<s.k-seq.k by RFUNCT_2:1;
  then 0<r-seq.k by SEQ_1:57;
  then 0+seq.k<r by XREAL_1:20;
  hence thesis;
end;

Lm5: (for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds f.r1<g1
) & seq is convergent & lim seq=x0 & rng seq c=dom f/\right_open_halfline(x0)
implies f/*seq is divergent_to-infty
proof
  assume that
A1: for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds f.
  r1<g1 and
A2: seq is convergent and
A3: lim seq=x0 and
A4: rng seq c=dom f/\right_open_halfline(x0);
A5: dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
  now
    let g1;
    consider r such that
A6: x0<r and
A7: for r1 st r1<r & x0<r1 & r1 in dom f holds f.r1<g1 by A1;
    consider n such that
A8: for k st n<=k holds seq.k<r by A2,A3,A6,Th2;
    take n;
    let k;
    assume
A9: n<=k;
A10: seq.k in rng seq by VALUED_0:28;
    then seq.k in right_open_halfline(x0) by A4,XBOOLE_0:def 4;
    then seq.k in {g2: x0<g2} by XXREAL_1:230;
    then
A11: ex g2 st g2=seq.k & x0<g2;
A12: k in NAT by ORDINAL1:def 12;
    seq.k in dom f by A4,A10,XBOOLE_0:def 4;
    then f.(seq.k)<g1 by A7,A8,A9,A11;
    hence (f/*seq).k<g1 by A4,A5,FUNCT_2:108,XBOOLE_1:1,A12;
  end;
  hence thesis;
end;

theorem Th3:
  0<r2 & ].r1-r2,r1.[ c= dom f implies for r st r<r1 ex g st r<g &
  g<r1 & g in dom f
proof
  assume that
A1: 0<r2 and
A2: ].r1-r2,r1.[c=dom f;
  let r such that
A3: r<r1;
  now
    per cases;
    suppose
A4:   r1-r2<=r;
      consider g being Real such that
A5:   r<g and
A6:   g<r1 by A3,XREAL_1:5;
      reconsider g as Real;
      take g;
      thus r<g & g<r1 by A5,A6;
      r1-r2<g by A4,A5,XXREAL_0:2;
      then g in {g2: r1-r2<g2 & g2<r1} by A6;
      then g in ].r1-r2,r1.[ by RCOMP_1:def 2;
      hence g in dom f by A2;
    end;
    suppose
A7:   r<=r1-r2;
      r1-r2<r1 by A1,Lm1;
      then consider g being Real such that
A8:   r1-r2<g and
A9:   g<r1 by XREAL_1:5;
      reconsider g as Real;
      take g;
      thus r<g & g<r1 by A7,A8,A9,XXREAL_0:2;
      g in {g2: r1-r2<g2 & g2<r1} by A8,A9;
      then g in ].r1-r2,r1.[ by RCOMP_1:def 2;
      hence g in dom f by A2;
    end;
  end;
  hence thesis;
end;

theorem Th4:
  0<r2 & ].r1,r1+r2.[ c= dom f implies for r st r1<r ex g st g<r &
  r1<g & g in dom f
proof
  assume that
A1: 0<r2 and
A2: ].r1,r1+r2.[ c=dom f;
  let r such that
A3: r1<r;
  now
    per cases;
    suppose
A4:   r1+r2<=r;
      r1<r1+r2 by A1,Lm1;
      then consider g being Real such that
A5:   r1<g and
A6:   g<r1+r2 by XREAL_1:5;
      reconsider g as Real;
      take g;
      thus g<r & r1<g by A4,A5,A6,XXREAL_0:2;
      g in {g2: r1<g2 & g2<r1+r2} by A5,A6;
      then g in ].r1,r1+r2.[ by RCOMP_1:def 2;
      hence g in dom f by A2;
    end;
    suppose
A7:   r<=r1+r2;
      consider g being Real such that
A8:   r1<g and
A9:   g<r by A3,XREAL_1:5;
      reconsider g as Real;
      take g;
      thus g<r & r1<g by A8,A9;
      g<r1+r2 by A7,A9,XXREAL_0:2;
      then g in {g2: r1<g2 & g2<r1+r2} by A8;
      then g in ].r1,r1+r2.[ by RCOMP_1:def 2;
      hence g in dom f by A2;
    end;
  end;
  hence thesis;
end;

theorem Th5:
  (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 & rng seq c= dom f /\
  left_open_halfline(x0)
proof
  deffunc U(Nat) = 1/($1+1);
  consider s1 be Real_Sequence such that
A1: for n holds s1.n=U(n) from SEQ_1:sch 1;
  reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
  set s2 = seq_const x0;
A2: s1 is convergent by A1,SEQ_4:31;
  then
A3: s2-s1 is convergent;
  assume
A4: for n holds x0-1/(n+1)<seq.n & seq.n<x0 & seq.n in dom f;
A5: now
    let n;
A6: (s2-s1).n=s2.n-s1.n by RFUNCT_2:1
      .=x0-s1.n by SEQ_1:57
      .=x0-1/(n+1) by A1;
    seq.n<=x0 by A4;
    hence (s2-s1).n<=seq.n & seq.n<=s2.n by A4,A6,SEQ_1:57;
  end;
  s2.0=x0 by SEQ_1:57;
  then
A7: lim s2=x0 by SEQ_4:25;
  lim s1=0 by A1,SEQ_4:31;
  then
A8: lim(s2-s1)=x0-0 by A7,A2,SEQ_2:12
    .=x0;
  hence seq is convergent by A7,A3,A5,SEQ_2:19;
  thus lim seq=x0 by A7,A3,A8,A5,SEQ_2:20;
  now
    let x be object;
    assume x in rng seq;
    then ex n being Element of NAT st seq.n=x by FUNCT_2:113;
    hence x in dom f by A4;
  end;
  hence
A9: rng seq c=dom f by TARSKI:def 3;
  now
    let x be object;
    assume x in rng seq;
    then consider n being Element of NAT such that
A10: x=seq.n by FUNCT_2:113;
    seq.n<x0 by A4;
    then seq.n in {g2:g2<x0};
    hence x in left_open_halfline(x0) by A10,XXREAL_1:229;
  end;
  then rng seq c=left_open_halfline(x0) by TARSKI:def 3;
  hence thesis by A9,XBOOLE_1:19;
end;

theorem Th6:
  (for n holds x0<seq.n & seq.n<x0+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 /\
  right_open_halfline(x0)
proof
  deffunc U(Nat) = 1/($1+1);
  consider s1 be Real_Sequence such that
A1: for n holds s1.n=U(n) from SEQ_1:sch 1;
  reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
  set s2 = seq_const x0;
A2: s1 is convergent by A1,SEQ_4:31;
  then
A3: s2+s1 is convergent;
  assume
A4: for n holds x0<seq.n & seq.n<x0+1/(n+1) & seq.n in dom f;
A5: now
    let n;
A6: (s2+s1).n=s2.n+s1.n by SEQ_1:7
      .=x0+s1.n by SEQ_1:57
      .=x0+1/(n+1) by A1;
    x0<=seq.n by A4;
    hence s2.n<=seq.n & seq.n<=(s2+s1).n by A4,A6,SEQ_1:57;
  end;
  s2.0=x0 by SEQ_1:57;
  then
A7: lim s2=x0 by SEQ_4:25;
  lim s1=0 by A1,SEQ_4:31;
  then
A8: lim(s2+s1)=x0+0 by A7,A2,SEQ_2:6
    .=x0;
  hence seq is convergent by A7,A3,A5,SEQ_2:19;
  thus lim seq=x0 by A7,A3,A8,A5,SEQ_2:20;
  now
    let x be object;
    assume x in rng seq;
    then ex n being Element of NAT st seq.n=x by FUNCT_2:113;
    hence x in dom f by A4;
  end;
  hence
A9: rng seq c=dom f by TARSKI:def 3;
  now
    let x be object;
    assume x in rng seq;
    then consider n being Element of NAT such that
A10: x=seq.n by FUNCT_2:113;
    x0<seq.n by A4;
    then seq.n in {g2:x0<g2};
    hence x in right_open_halfline(x0) by A10,XXREAL_1:230;
  end;
  then rng seq c=right_open_halfline(x0) by TARSKI:def 3;
  hence thesis by A9,XBOOLE_1:19;
end;

definition
  let f,x0;
  pred f is_left_convergent_in x0 means

  (for r st r<x0 ex g st r<g & g<
x0 & g in dom f) & ex g st for seq st seq is convergent & lim seq=x0 & rng seq
c= dom f /\ left_open_halfline(x0) holds f/*seq is convergent & lim(f/*seq)=g;
  pred f is_left_divergent_to+infty_in x0 means

  (for r st r<x0 ex g st
r<g & g<x0 & g in dom f) & for seq st seq is convergent & lim seq=x0 & rng seq
  c= dom f /\ left_open_halfline(x0) holds f/*seq is divergent_to+infty;
  pred f is_left_divergent_to-infty_in x0 means

  (for r st r<x0 ex g st
r<g & g<x0 & g in dom f) & for seq st seq is convergent & lim seq=x0 & rng seq
  c= dom f /\ left_open_halfline(x0) holds f/*seq is divergent_to-infty;
  pred f is_right_convergent_in x0 means

  (for r st x0<r ex g st g<r &
  x0<g & g in dom f) & ex g st for seq st seq is convergent & lim seq=x0 & rng
seq c= dom f /\ right_open_halfline(x0) holds f/*seq is convergent & lim(f/*seq
  )=g;
  pred f is_right_divergent_to+infty_in x0 means

  (for r st x0<r ex g st
g<r & x0<g & g in dom f) & for seq st seq is convergent & lim seq=x0 & rng seq
  c= dom f /\ right_open_halfline(x0) holds f/*seq is divergent_to+infty;
  pred f is_right_divergent_to-infty_in x0 means

  (for r st x0<r ex g st
g<r & x0<g & g in dom f) & for seq st seq is convergent & lim seq=x0 & rng seq
  c= dom f /\ right_open_halfline(x0) holds f/*seq is divergent_to-infty;
end;

theorem
  f is_left_convergent_in x0 iff (for r st r<x0 ex g st r<g & g<x0 & g
  in dom f) & ex g st for g1 st 0<g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1
  in dom f holds |.f.r1-g.|<g1
proof
  thus f is_left_convergent_in x0 implies (for r st r<x0 ex g st r<g & g<x0 &
g in dom f) & ex g st for g1 st 0<g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1
  in dom f holds |.f.r1-g.|<g1
  proof
    assume that
A1: f is_left_convergent_in x0 and
A2: (not for r st r<x0 ex g st r<g & g<x0 & g in dom f) or for g ex g1
st 0<g1 & for r st r<x0 ex r1 st r<r1 & r1<x0 & 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/\
left_open_halfline(x0) holds f/*seq is convergent & lim(f/*seq)=g by A1;
    consider g1 such that
A4: 0<g1 and
A5: for r st r<x0 ex r1 st r<r1 & r1<x0 & r1 in dom f & |.f.r1-g.|>=
    g1 by A1,A2;
    defpred X[Nat,Real] means x0-1/($1+1)<$2 & $2<x0 & $2 in
    dom f & |.f.($2)-g.|>=g1;
A6: now
      let n be Element of NAT;
      x0-1/(n+1)<x0 by Lm3;
      then consider g2 such that
A7:   x0-1/(n+1)<g2 and
A8:   g2<x0 and
A9:   g2 in dom f and
A10:  |.f.g2-g.|>=g1 by A5;
       reconsider g2 as Element of REAL by XREAL_0:def 1;
      take g2;
      thus X[n,g2] by A7,A8,A9,A10;
    end;
    consider s be Real_Sequence such that
A11: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A6);
A12: for n being Nat holds X[n,s.n]
     proof let n;
      n in NAT by ORDINAL1:def 12;
      hence thesis by A11;
     end;
A13: rng s c=dom f/\left_open_halfline(x0) by A12,Th5;
A14: lim s=x0 by A12,Th5;
A15: s is convergent by A12,Th5;
    then
A16: lim(f/*s)=g by A3,A14,A13;
    f/*s is convergent by A3,A15,A14,A13;
    then consider n such that
A17: for k st n<=k holds |.(f/*s).k-g.|<g1 by A4,A16,SEQ_2:def 7;
A18: |.(f/*s).n-g.|<g1 by A17;
A19: n in NAT by ORDINAL1:def 12;
    rng s c=dom f by A12,Th5;
    then |.f.(s.n)-g.|<g1 by A18,FUNCT_2:108,A19;
    hence contradiction by A12;
  end;
  assume
A20: for r st r<x0 ex g st r<g & g<x0 & g in dom f;
  given g such that
A21: for g1 st 0<g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f
  holds |.f.r1-g.|<g1;
  now
    let s be Real_Sequence such that
A22: s is convergent and
A23: lim s=x0 and
A24: rng s c=dom f/\left_open_halfline(x0);
A25: dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
A26: now
      let g1 be Real;
      assume
A27:  0<g1;
      consider r such that
A28:  r<x0 and
A29:  for r1 st r<r1 & r1<x0 & r1 in dom f holds |.f.r1-g.|<g1 by A21,A27;
      consider n such that
A30:  for k st n<=k holds r<s.k by A22,A23,A28,Th1;
      take n;
      let k;
      assume
A31:  n<=k;
A32:  s.k in rng s by VALUED_0:28;
      then s.k in left_open_halfline(x0) by A24,XBOOLE_0:def 4;
      then s.k in {g2: g2<x0} by XXREAL_1:229;
      then
A33:  ex g2 st g2=s.k & g2<x0;
A34: k in NAT by ORDINAL1:def 12;
      s.k in dom f by A24,A32,XBOOLE_0:def 4;
      then |.f.(s.k)-g.|<g1 by A29,A30,A31,A33;
      hence |.(f/*s).k-g.|<g1 by A24,A25,FUNCT_2:108,XBOOLE_1:1,A34;
    end;
    hence f/*s is convergent by SEQ_2:def 6;
    hence lim(f/*s)=g by A26,SEQ_2:def 7;
  end;
  hence thesis by A20;
end;

theorem
  f is_left_divergent_to+infty_in x0 iff (for r st r<x0 ex g st r<g & g<
  x0 & g in dom f) & for g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f
  holds g1<f.r1
proof
  thus f is_left_divergent_to+infty_in x0 implies (for r st r<x0 ex g st r<g &
g<x0 & g in dom f) & for g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f
  holds g1<f.r1
  proof
    assume that
A1: f is_left_divergent_to+infty_in x0 and
A2: (not for r st r<x0 ex g st r<g & g<x0 & g in dom f) or ex g1 st
    for r st r<x0 ex r1 st r<r1 & r1<x0 & r1 in dom f & g1>=f.r1;
    consider g1 such that
A3: for r st r<x0 ex r1 st r<r1 & r1<x0 & r1 in dom f & g1>=f.r1 by A1,A2;
    defpred X[Nat,Real] means x0-1/($1+1)<$2 & $2<x0 & $2 in
    dom f & f.($2)<=g1;
A4: now
      let n be Element of NAT;
      x0-1/(n+1)<x0 by Lm3;
      then consider g2 such that
A5:   x0-1/(n+1)<g2 and
A6:   g2<x0 and
A7:   g2 in dom f and
A8:   f.g2<=g1 by A3;
       reconsider g2 as Element of REAL by XREAL_0:def 1;
      take g2;
      thus X[n,g2] by A5,A6,A7,A8;
    end;
    consider s be Real_Sequence such that
A9: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A4);
A10: for n being Nat holds X[n,s.n]
     proof let n be Nat;
      n in NAT by ORDINAL1:def 12;
      hence thesis by A9;
     end;
A11: rng s c=dom f/\left_open_halfline(x0) by A10,Th5;
A12: lim s=x0 by A10,Th5;
    s is convergent by A10,Th5;
    then f/*s is divergent_to+infty by A1,A12,A11;
    then consider n such that
A13: for k st n<=k holds g1<(f/*s).k;
A14: g1<(f/*s).n by A13;
A15: n in NAT by ORDINAL1:def 12;
    rng s c=dom f by A10,Th5;
    then g1<f.(s.n) by A14,FUNCT_2:108,A15;
    hence contradiction by A10;
  end;
  assume that
A16: for r st r<x0 ex g st r<g & g<x0 & g in dom f and
A17: for g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds g1 <f.r1;
  now
    let s be Real_Sequence such that
A18: s is convergent and
A19: lim s=x0 and
A20: rng s c=dom f/\left_open_halfline(x0);
A21: dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
    now
      let g1;
      consider r such that
A22:  r<x0 and
A23:  for r1 st r<r1 & r1<x0 & r1 in dom f holds g1<f.r1 by A17;
      consider n such that
A24:  for k st n<=k holds r<s.k by A18,A19,A22,Th1;
      take n;
      let k;
      assume
A25:  n<=k;
A26:  s.k in rng s by VALUED_0:28;
      then s.k in left_open_halfline(x0) by A20,XBOOLE_0:def 4;
      then s.k in {g2: g2<x0} by XXREAL_1:229;
      then
A27:  ex g2 st g2=s.k & g2<x0;
A28: k in NAT by ORDINAL1:def 12;
      s.k in dom f by A20,A26,XBOOLE_0:def 4;
      then g1<f.(s.k) by A23,A24,A25,A27;
      hence g1<(f/*s).k by A20,A21,FUNCT_2:108,XBOOLE_1:1,A28;
    end;
    hence f/*s is divergent_to+infty;
  end;
  hence thesis by A16;
end;

theorem
  f is_left_divergent_to-infty_in x0 iff (for r st r<x0 ex g st r<g & g<
  x0 & g in dom f) & for g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f
  holds f.r1<g1
proof
  thus f is_left_divergent_to-infty_in x0 implies (for r st r<x0 ex g st r<g &
g<x0 & g in dom f) & for g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f
  holds f.r1<g1
  proof
    assume that
A1: f is_left_divergent_to-infty_in x0 and
A2: (not for r st r<x0 ex g st r<g & g<x0 & g in dom f) or ex g1 st
    for r st r<x0 ex r1 st r<r1 & r1<x0 & r1 in dom f & g1<=f.r1;
    consider g1 such that
A3: for r st r<x0 ex r1 st r<r1 & r1<x0 & r1 in dom f & g1<=f.r1 by A1,A2;
    defpred X[Nat,Real] means x0-1/($1+1)<$2 & $2<x0 & $2 in
    dom f & g1<=f.($2);
A4: now
      let n be Element of NAT;
      x0-1/(n+1)<x0 by Lm3;
      then consider g2 such that
A5:   x0-1/(n+1)<g2 and
A6:   g2<x0 and
A7:   g2 in dom f and
A8:   g1<=f.g2 by A3;
       reconsider g2 as Element of REAL by XREAL_0:def 1;
      take g2;
      thus X[n,g2] by A5,A6,A7,A8;
    end;
    consider s be Real_Sequence such that
A9: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A4);
A10: for n being Nat holds X[n,s.n]
     proof let n;
      n in NAT by ORDINAL1:def 12;
      hence thesis by A9;
     end;
A11: rng s c=dom f/\left_open_halfline(x0) by A10,Th5;
A12: lim s=x0 by A10,Th5;
    s is convergent by A10,Th5;
    then f/*s is divergent_to-infty by A1,A12,A11;
    then consider n such that
A13: for k st n<=k holds (f/*s).k<g1;
A14: (f/*s).n<g1 by A13;
A15: n in NAT by ORDINAL1:def 12;
    rng s c=dom f by A10,Th5;
    then f.(s.n)<g1 by A14,FUNCT_2:108,A15;
    hence contradiction by A10;
  end;
  assume that
A16: for r st r<x0 ex g st r<g & g<x0 & g in dom f and
A17: for g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds f. r1<g1;
  now
    let s be Real_Sequence such that
A18: s is convergent and
A19: lim s=x0 and
A20: rng s c=dom f/\left_open_halfline(x0);
A21: dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
    now
      let g1;
      consider r such that
A22:  r<x0 and
A23:  for r1 st r<r1 & r1<x0 & r1 in dom f holds f.r1<g1 by A17;
      consider n such that
A24:  for k st n<=k holds r<s.k by A18,A19,A22,Th1;
      take n;
      let k;
      assume
A25:  n<=k;
A26:  s.k in rng s by VALUED_0:28;
      then s.k in left_open_halfline(x0) by A20,XBOOLE_0:def 4;
      then s.k in {g2: g2<x0} by XXREAL_1:229;
      then
A27:  ex g2 st g2=s.k & g2<x0;
A28: k in NAT by ORDINAL1:def 12;
      s.k in dom f by A20,A26,XBOOLE_0:def 4;
      then f.(s.k)<g1 by A23,A24,A25,A27;
      hence (f/*s).k<g1 by A20,A21,FUNCT_2:108,XBOOLE_1:1,A28;
    end;
    hence f/*s is divergent_to-infty;
  end;
  hence thesis by A16;
end;

theorem
  f is_right_convergent_in x0 iff (for r st x0<r ex g st g<r & x0<g & g
  in dom f) & ex g st for g1 st 0<g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1
  in dom f holds |.f.r1-g.|<g1
proof
  thus f is_right_convergent_in x0 implies (for r st x0<r ex g st g<r & x0<g &
g in dom f) & ex g st for g1 st 0<g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1
  in dom f holds |.f.r1-g.|<g1
  proof
    assume that
A1: f is_right_convergent_in x0 and
A2: (not for r st x0<r ex g st g<r & x0<g & g in dom f) or for g ex g1
st 0<g1 & for r st x0<r ex r1 st r1<r & x0<r1 & 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/\
right_open_halfline(x0) holds f/*seq is convergent & lim(f/*seq)=g by A1;
    consider g1 such that
A4: 0<g1 and
A5: for r st x0<r ex r1 st r1<r & x0<r1 & r1 in dom f & |.f.r1-g.|>=
    g1 by A1,A2;
    defpred X[Nat,Real] means x0<$2 & $2<x0+1/($1+1) & $2 in
    dom f & g1<=|.f.($2)-g.|;
A6: now
      let n be Element of NAT;
      x0<x0+1/(n+1) by Lm3;
      then consider r1 such that
A7:   r1<x0+(1/(n+1)) and
A8:   x0<r1 and
A9:   r1 in dom f and
A10:  g1<=|.f.r1-g.| by A5;
       reconsider r1 as Element of REAL by XREAL_0:def 1;
      take r1;
      thus X[n,r1] by A7,A8,A9,A10;
    end;
    consider s be Real_Sequence such that
A11: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A6);
A12: for n being Nat holds X[n,s.n]
     proof let n;
      n in NAT by ORDINAL1:def 12;
      hence thesis by A11;
     end;
A13: rng s c=dom f/\right_open_halfline(x0) by A12,Th6;
A14: lim s=x0 by A12,Th6;
A15: s is convergent by A12,Th6;
    then
A16: lim(f/*s)=g by A3,A14,A13;
    f/*s is convergent by A3,A15,A14,A13;
    then consider n such that
A17: for k st n<=k holds |.(f/*s).k-g.|<g1 by A4,A16,SEQ_2:def 7;
A18: |.(f/*s).n-g.|<g1 by A17;
A19: n in NAT by ORDINAL1:def 12;
    rng s c=dom f by A12,Th6;
    then |.f.(s.n)-g.|<g1 by A18,FUNCT_2:108,A19;
    hence contradiction by A12;
  end;
  assume
A20: for r st x0<r ex g st g<r & x0<g & g in dom f;
  given g such that
A21: for g1 st 0<g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f
  holds |.f.r1-g.|<g1;
  now
    let s be Real_Sequence such that
A22: s is convergent and
A23: lim s=x0 and
A24: rng s c=dom f/\right_open_halfline(x0);
A25: dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
A26: now
      let g1 be Real;
      assume
A27:  0<g1;
      consider r such that
A28:  x0<r and
A29:  for r1 st r1<r & x0<r1 & r1 in dom f holds |.f.r1-g.|<g1 by A21,A27;
      consider n such that
A30:  for k st n<=k holds s.k<r by A22,A23,A28,Th2;
      take n;
      let k;
      assume
A31:  n<=k;
A32:  s.k in rng s by VALUED_0:28;
      then s.k in right_open_halfline(x0) by A24,XBOOLE_0:def 4;
      then s.k in {g2: x0<g2} by XXREAL_1:230;
      then
A33:  ex g2 st g2=s.k & x0<g2;
A34: k in NAT by ORDINAL1:def 12;
      s.k in dom f by A24,A32,XBOOLE_0:def 4;
      then |.f.(s.k)-g.|<g1 by A29,A30,A31,A33;
      hence |.(f/*s).k-g.|<g1 by A24,A25,FUNCT_2:108,XBOOLE_1:1,A34;
    end;
    hence f/*s is convergent by SEQ_2:def 6;
    hence lim(f/*s)=g by A26,SEQ_2:def 7;
  end;
  hence thesis by A20;
end;

theorem
  f is_right_divergent_to+infty_in x0 iff (for r st x0<r ex g st g<r &
x0<g & g in dom f) & for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f
  holds g1<f.r1
proof
  thus f is_right_divergent_to+infty_in x0 implies (for r st x0<r ex g st g<r
& x0<g & g in dom f) & for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom
  f holds g1<f.r1
  proof
    assume that
A1: f is_right_divergent_to+infty_in x0 and
A2: (not for r st x0<r ex g st g<r & x0<g & g in dom f) or ex g1 st
    for r st x0<r ex r1 st r1<r & x0<r1 & r1 in dom f & f.r1<=g1;
    consider g1 such that
A3: for r st x0<r ex r1 st r1<r & x0<r1 & r1 in dom f & f.r1<=g1 by A1,A2;
    defpred X[Nat,Real] means x0<$2 & $2<x0+1/($1+1) & $2 in
    dom f & f.($2)<=g1;
A4: now
      let n be Element of NAT;
      x0<x0+1/(n+1) by Lm3;
      then consider r1 such that
A5:   r1<x0+(1/(n+1)) and
A6:   x0<r1 and
A7:   r1 in dom f and
A8:   f.r1<=g1 by A3;
       reconsider r1 as Element of REAL by XREAL_0:def 1;
      take r1;
      thus X[n,r1] by A5,A6,A7,A8;
    end;
    consider s be Real_Sequence such that
A9: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A4);
A10: for n being Nat holds X[n,s.n]
     proof let n;
      n in NAT by ORDINAL1:def 12;
      hence thesis by A9;
     end;
A11: rng s c=dom f/\right_open_halfline(x0) by A10,Th6;
A12: lim s=x0 by A10,Th6;
    s is convergent by A10,Th6;
    then f/*s is divergent_to+infty by A1,A12,A11;
    then consider n such that
A13: for k st n<=k holds g1<(f/*s).k;
A14: g1<(f/*s).n by A13;
A15: n in NAT by ORDINAL1:def 12;
    rng s c=dom f by A10,Th6;
    then g1<f.(s.n) by A14,FUNCT_2:108,A15;
    hence contradiction by A10;
  end;
  assume that
A16: for r st x0<r ex g st g<r & x0<g & g in dom f and
A17: for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds g1 <f.r1;
  now
    let s be Real_Sequence such that
A18: s is convergent and
A19: lim s=x0 and
A20: rng s c=dom f/\right_open_halfline(x0);
A21: dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
    now
      let g1;
      consider r such that
A22:  x0<r and
A23:  for r1 st r1<r & x0<r1 & r1 in dom f holds g1<f.r1 by A17;
      consider n such that
A24:  for k st n<=k holds s.k<r by A18,A19,A22,Th2;
      take n;
      let k;
      assume
A25:  n<=k;
A26:  s.k in rng s by VALUED_0:28;
      then s.k in right_open_halfline(x0) by A20,XBOOLE_0:def 4;
      then s.k in {g2: x0<g2} by XXREAL_1:230;
      then
A27:  ex g2 st g2=s.k & x0<g2;
A28: k in NAT by ORDINAL1:def 12;
      s.k in dom f by A20,A26,XBOOLE_0:def 4;
      then g1<f.(s.k) by A23,A24,A25,A27;
      hence g1<(f/*s).k by A20,A21,FUNCT_2:108,XBOOLE_1:1,A28;
    end;
    hence f/*s is divergent_to+infty;
  end;
  hence thesis by A16;
end;

theorem
  f is_right_divergent_to-infty_in x0 iff (for r st x0<r ex g st g<r &
x0<g & g in dom f) & for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f
  holds f.r1<g1
proof
  thus f is_right_divergent_to-infty_in x0 implies (for r st x0<r ex g st g<r
& x0<g & g in dom f) & for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom
  f holds f.r1<g1
  proof
    assume that
A1: f is_right_divergent_to-infty_in x0 and
A2: (not for r st x0<r ex g st g<r & x0<g & g in dom f) or ex g1 st
    for r st x0<r ex r1 st r1<r & x0<r1 & r1 in dom f & g1<=f.r1;
    consider g1 such that
A3: for r st x0<r ex r1 st r1<r & x0<r1 & r1 in dom f & g1<=f.r1 by A1,A2;
    defpred X[Nat,Real] means x0<$2 & $2<x0+1/($1+1) & $2 in
    dom f & g1<=f.($2);
A4: now
      let n be Element of NAT;
      x0<x0+1/(n+1) by Lm3;
      then consider r1 such that
A5:   r1<x0+(1/(n+1)) and
A6:   x0<r1 and
A7:   r1 in dom f and
A8:   g1<=f.r1 by A3;
       reconsider r1 as Element of REAL by XREAL_0:def 1;
      take r1;
      thus X[n,r1] by A5,A6,A7,A8;
    end;
    consider s be Real_Sequence such that
A9: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A4);
A10: for n being Nat holds X[n,s.n]
     proof let n;
      n in NAT by ORDINAL1:def 12;
      hence thesis by A9;
     end;
A11: rng s c=dom f/\right_open_halfline(x0) by A10,Th6;
A12: lim s=x0 by A10,Th6;
    s is convergent by A10,Th6;
    then f/*s is divergent_to-infty by A1,A12,A11;
    then consider n such that
A13: for k st n<=k holds (f/*s).k<g1;
A14: (f/*s).n<g1 by A13;
A15: n in NAT by ORDINAL1:def 12;
    rng s c=dom f by A10,Th6;
    then f.(s.n)<g1 by A14,FUNCT_2:108,A15;
    hence contradiction by A10;
  end;
  assume that
A16: for r st x0<r ex g st g<r & x0<g & g in dom f and
A17: for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds f. r1<g1;
  for s be Real_Sequence holds s is convergent & lim s=x0 & rng s c=dom f
  /\right_open_halfline(x0) implies f/*s is divergent_to-infty by A17,Lm5;
  hence thesis by A16;
end;

theorem
  f1 is_left_divergent_to+infty_in x0 & f2 is_left_divergent_to+infty_in
  x0 & (for r st r<x0 ex g st r<g & g<x0 & g in dom f1 /\ dom f2) implies f1+f2
  is_left_divergent_to+infty_in x0 & f1(#) f2 is_left_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_left_divergent_to+infty_in x0 and
A2: f2 is_left_divergent_to+infty_in x0 and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom f1/\dom f2;
A4: now
    let seq;
    assume that
A5: seq is convergent and
A6: lim seq=x0 and
A7: rng seq c=dom(f1+f2)/\left_open_halfline(x0);
    rng seq c=dom f2/\left_open_halfline(x0) by A7,Lm4;
    then
A8: f2/*seq is divergent_to+infty by A2,A5,A6;
    rng seq c=dom f1/\left_open_halfline(x0) by A7,Lm4;
    then f1/*seq is divergent_to+infty by A1,A5,A6;
    then
A9: f1/*seq+f2/*seq is divergent_to+infty by A8,LIMFUNC1:8;
A10: dom(f1+f2)=dom f1/\dom f2 by A7,Lm4;
    rng seq c=dom(f1+f2) by A7,Lm4;
    hence (f1+f2)/*seq is divergent_to+infty by A10,A9,RFUNCT_2:8;
  end;
A11: now
    let seq;
    assume that
A12: seq is convergent and
A13: lim seq=x0 and
A14: rng seq c=dom(f1(#)f2)/\left_open_halfline(x0);
    rng seq c=dom f2/\left_open_halfline(x0) by A14,Lm2;
    then
A15: f2/*seq is divergent_to+infty by A2,A12,A13;
    rng seq c=dom f1/\left_open_halfline(x0) by A14,Lm2;
    then f1/*seq is divergent_to+infty by A1,A12,A13;
    then
A16: (f1/*seq)(#)(f2/*seq) is divergent_to+infty by A15,LIMFUNC1:10;
A17: dom(f1(#)f2)=dom f1/\dom f2 by A14,Lm2;
    rng seq c=dom(f1(#)f2) by A14,Lm2;
    hence (f1(#)f2)/*seq is divergent_to+infty by A17,A16,RFUNCT_2:8;
  end;
  now
    let r;
    assume r<x0;
    then consider g such that
A18: r<g and
A19: g<x0 and
A20: g in dom f1/\dom f2 by A3;
    take g;
    thus r<g & g<x0 & g in dom(f1+f2) by A18,A19,A20,VALUED_1:def 1;
  end;
  hence f1+f2 is_left_divergent_to+infty_in x0 by A4;
  now
    let r;
    assume r<x0;
    then consider g such that
A21: r<g and
A22: g<x0 and
A23: g in dom f1/\dom f2 by A3;
    take g;
    thus r<g & g<x0 & g in dom(f1(#)f2) by A21,A22,A23,VALUED_1:def 4;
  end;
  hence thesis by A11;
end;

theorem
  f1 is_left_divergent_to-infty_in x0 & f2 is_left_divergent_to-infty_in
  x0 & (for r st r<x0 ex g st r<g & g<x0 & g in dom f1 /\ dom f2) implies f1+f2
  is_left_divergent_to-infty_in x0 & f1(#)f2 is_left_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_left_divergent_to-infty_in x0 and
A2: f2 is_left_divergent_to-infty_in x0 and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom f1/\dom f2;
A4: now
    let seq;
    assume that
A5: seq is convergent and
A6: lim seq=x0 and
A7: rng seq c=dom(f1+f2)/\left_open_halfline(x0);
    rng seq c=dom f2/\left_open_halfline(x0) by A7,Lm4;
    then
A8: f2/*seq is divergent_to-infty by A2,A5,A6;
    rng seq c=dom f1/\left_open_halfline(x0) by A7,Lm4;
    then f1/*seq is divergent_to-infty by A1,A5,A6;
    then
A9: f1/*seq+f2/*seq is divergent_to-infty by A8,LIMFUNC1:11;
A10: dom(f1+f2)=dom f1/\dom f2 by A7,Lm4;
    rng seq c=dom(f1+f2) by A7,Lm4;
    hence (f1+f2)/*seq is divergent_to-infty by A10,A9,RFUNCT_2:8;
  end;
A11: now
    let seq;
    assume that
A12: seq is convergent and
A13: lim seq=x0 and
A14: rng seq c=dom(f1(#)f2)/\left_open_halfline(x0);
    rng seq c=dom f2/\left_open_halfline(x0) by A14,Lm2;
    then
A15: f2/*seq is divergent_to-infty by A2,A12,A13;
    rng seq c=dom f1/\left_open_halfline(x0) by A14,Lm2;
    then f1/*seq is divergent_to-infty by A1,A12,A13;
    then
A16: (f1/*seq)(#)(f2/*seq) is divergent_to+infty by A15,LIMFUNC1:24;
A17: dom(f1(#)f2)=dom f1/\dom f2 by A14,Lm2;
    rng seq c=dom(f1(#)f2) by A14,Lm2;
    hence (f1(#)f2)/*seq is divergent_to+infty by A17,A16,RFUNCT_2:8;
  end;
  now
    let r;
    assume r<x0;
    then consider g such that
A18: r<g and
A19: g<x0 and
A20: g in dom f1/\dom f2 by A3;
    take g;
    thus r<g & g<x0 & g in dom(f1+f2) by A18,A19,A20,VALUED_1:def 1;
  end;
  hence f1+f2 is_left_divergent_to-infty_in x0 by A4;
  now
    let r;
    assume r<x0;
    then consider g such that
A21: r<g and
A22: g<x0 and
A23: g in dom f1/\dom f2 by A3;
    take g;
    thus r<g & g<x0 & g in dom(f1(#)f2) by A21,A22,A23,VALUED_1:def 4;
  end;
  hence thesis by A11;
end;

theorem
  f1 is_right_divergent_to+infty_in x0 & f2
  is_right_divergent_to+infty_in x0 & (for r st x0<r ex g st g<r & x0<g & g in
  dom f1 /\ dom f2) implies f1+f2 is_right_divergent_to+infty_in x0 & f1(#)f2
  is_right_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_right_divergent_to+infty_in x0 and
A2: f2 is_right_divergent_to+infty_in x0 and
A3: for r st x0<r ex g st g<r & x0<g & g in dom f1/\dom f2;
A4: now
    let seq;
    assume that
A5: seq is convergent and
A6: lim seq=x0 and
A7: rng seq c=dom(f1+f2)/\right_open_halfline(x0);
    rng seq c=dom f2/\right_open_halfline(x0) by A7,Lm4;
    then
A8: f2/*seq is divergent_to+infty by A2,A5,A6;
    rng seq c=dom f1/\right_open_halfline(x0) by A7,Lm4;
    then f1/*seq is divergent_to+infty by A1,A5,A6;
    then
A9: f1/*seq+f2/*seq is divergent_to+infty by A8,LIMFUNC1:8;
A10: dom(f1+f2)=dom f1/\dom f2 by A7,Lm4;
    rng seq c=dom(f1+f2) by A7,Lm4;
    hence (f1+f2)/*seq is divergent_to+infty by A10,A9,RFUNCT_2:8;
  end;
A11: now
    let seq;
    assume that
A12: seq is convergent and
A13: lim seq=x0 and
A14: rng seq c=dom(f1(#)f2)/\right_open_halfline(x0);
    rng seq c=dom f2/\right_open_halfline(x0) by A14,Lm2;
    then
A15: f2/*seq is divergent_to+infty by A2,A12,A13;
    rng seq c=dom f1/\right_open_halfline(x0) by A14,Lm2;
    then f1/*seq is divergent_to+infty by A1,A12,A13;
    then
A16: (f1/*seq)(#)(f2/*seq) is divergent_to+infty by A15,LIMFUNC1:10;
A17: dom(f1(#)f2)=dom f1/\dom f2 by A14,Lm2;
    rng seq c=dom(f1(#)f2) by A14,Lm2;
    hence (f1(#)f2)/*seq is divergent_to+infty by A17,A16,RFUNCT_2:8;
  end;
  now
    let r;
    assume x0<r;
    then consider g such that
A18: g<r and
A19: x0<g and
A20: g in dom f1/\dom f2 by A3;
    take g;
    thus g<r & x0<g & g in dom(f1+f2) by A18,A19,A20,VALUED_1:def 1;
  end;
  hence f1+f2 is_right_divergent_to+infty_in x0 by A4;
  now
    let r;
    assume x0<r;
    then consider g such that
A21: g<r and
A22: x0<g and
A23: g in dom f1/\dom f2 by A3;
    take g;
    thus g<r & x0<g & g in dom(f1(#)f2) by A21,A22,A23,VALUED_1:def 4;
  end;
  hence thesis by A11;
end;

theorem
  f1 is_right_divergent_to-infty_in x0 & f2
  is_right_divergent_to-infty_in x0 & (for r st x0<r ex g st g<r & x0<g & g in
  dom f1 /\ dom f2) implies f1+f2 is_right_divergent_to-infty_in x0 & f1(#)f2
  is_right_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_right_divergent_to-infty_in x0 and
A2: f2 is_right_divergent_to-infty_in x0 and
A3: for r st x0<r ex g st g<r & x0<g & g in dom f1/\dom f2;
A4: now
    let seq;
    assume that
A5: seq is convergent and
A6: lim seq=x0 and
A7: rng seq c=dom(f1+f2)/\right_open_halfline(x0);
    rng seq c=dom f2/\right_open_halfline(x0) by A7,Lm4;
    then
A8: f2/*seq is divergent_to-infty by A2,A5,A6;
    rng seq c=dom f1/\right_open_halfline(x0) by A7,Lm4;
    then f1/*seq is divergent_to-infty by A1,A5,A6;
    then
A9: f1/*seq+f2/*seq is divergent_to-infty by A8,LIMFUNC1:11;
A10: dom(f1+f2)=dom f1/\dom f2 by A7,Lm4;
    rng seq c=dom(f1+f2) by A7,Lm4;
    hence (f1+f2)/*seq is divergent_to-infty by A10,A9,RFUNCT_2:8;
  end;
A11: now
    let seq;
    assume that
A12: seq is convergent and
A13: lim seq=x0 and
A14: rng seq c=dom(f1(#)f2)/\right_open_halfline(x0);
    rng seq c=dom f2/\right_open_halfline(x0) by A14,Lm2;
    then
A15: f2/*seq is divergent_to-infty by A2,A12,A13;
    rng seq c=dom f1/\right_open_halfline(x0) by A14,Lm2;
    then f1/*seq is divergent_to-infty by A1,A12,A13;
    then
A16: (f1/*seq)(#)(f2/*seq) is divergent_to+infty by A15,LIMFUNC1:24;
A17: dom(f1(#)f2)=dom f1/\dom f2 by A14,Lm2;
    rng seq c=dom(f1(#)f2) by A14,Lm2;
    hence (f1(#)f2)/*seq is divergent_to+infty by A17,A16,RFUNCT_2:8;
  end;
  now
    let r;
    assume x0<r;
    then consider g such that
A18: g<r and
A19: x0<g and
A20: g in dom f1/\dom f2 by A3;
    take g;
    thus g<r & x0<g & g in dom(f1+f2) by A18,A19,A20,VALUED_1:def 1;
  end;
  hence f1+f2 is_right_divergent_to-infty_in x0 by A4;
  now
    let r;
    assume x0<r;
    then consider g such that
A21: g<r and
A22: x0<g and
A23: g in dom f1/\dom f2 by A3;
    take g;
    thus g<r & x0<g & g in dom(f1(#)f2) by A21,A22,A23,VALUED_1:def 4;
  end;
  hence thesis by A11;
end;

theorem
  f1 is_left_divergent_to+infty_in x0 & (for r st r<x0 ex g st r<g & g<
x0 & g in dom(f1+f2)) & (ex r st 0<r & f2|].x0-r,x0.[ is bounded_below) implies
  f1+f2 is_left_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_left_divergent_to+infty_in x0 and
A2: for r st r<x0 ex g st r<g & g<x0 & g in dom(f1+f2);
  given r such that
A3: 0<r and
A4: f2|].x0-r,x0.[ is bounded_below;
  now
    let seq such that
A5: seq is convergent and
A6: lim seq=x0 and
A7: rng seq c=dom(f1+f2)/\left_open_halfline(x0);
    x0-r<x0 by A3,Lm1;
    then consider k such that
A8: for n st k<=n holds x0-r<seq.n by A5,A6,Th1;
A9: dom(f1+f2)/\left_open_halfline(x0) c=dom(f1+f2) by XBOOLE_1:17;
    rng(seq^\k)c=rng seq by VALUED_0:21;
    then
A10: rng(seq^\k)c=dom(f1+f2)/\left_open_halfline(x0) by A7,XBOOLE_1:1;
    then
A11: rng(seq^\k)c=dom(f1+f2) by A9,XBOOLE_1:1;
A12: dom(f1+f2)=dom f1/\dom f2 by VALUED_1:def 1;
    then
A13: dom(f1+f2)c=dom f2 by XBOOLE_1:17;
    then
A14: rng(seq^\k)c=dom f2 by A11,XBOOLE_1:1;
    dom(f1+f2)c=dom f1 by A12,XBOOLE_1:17;
    then
A15: rng(seq^\k)c=dom f1 by A11,XBOOLE_1:1;
    then rng(seq^\k)c=dom f1/\dom f2 by A14,XBOOLE_1:19;
    then
A16: f1/*(seq^\k)+f2/*(seq^\k)=(f1+f2)/*(seq^\k) by RFUNCT_2:8
      .=((f1+f2)/*seq)^\k by A7,A9,VALUED_0:27,XBOOLE_1:1;
    dom(f1+f2)/\left_open_halfline(x0) c=left_open_halfline(x0) by XBOOLE_1:17;
    then
A17: rng(seq^\k)c=left_open_halfline(x0) by A10,XBOOLE_1:1;
    then
A18: rng(seq^\k)c=dom f1/\left_open_halfline(x0) by A15,XBOOLE_1:19;
    now
      consider r1 be Real such that
A19:  for g being object st g in ].x0-r,x0.[/\dom f2 holds r1<=f2.g by A4,
RFUNCT_1:71;
      take r2=r1-1;
      let n;
A20: n in NAT by ORDINAL1:def 12;
      x0-r<seq.(n+k) by A8,NAT_1:12;
      then
A21:  x0-r<(seq^\k).n by NAT_1:def 3;
A22:  (seq^\k).n in rng(seq^\k) by VALUED_0:28;
      then (seq^\k).n in left_open_halfline(x0) by A17;
      then (seq^\k).n in {g1: g1<x0} by XXREAL_1:229;
      then ex g st g=(seq^\k).n & g<x0;
      then (seq^\k).n in {g2: x0-r<g2 & g2<x0} by A21;
      then (seq^\k).n in ].x0-r,x0.[ by RCOMP_1:def 2;
      then (seq^\k).n in ].x0-r,x0.[/\dom f2 by A14,A22,XBOOLE_0:def 4;
      then r1-1<f2.((seq^\k).n)-0 by A19,XREAL_1:15;
      hence r2<(f2/*(seq^\k)).n by A11,A13,FUNCT_2:108,XBOOLE_1:1,A20;
    end;
    then
A23: f2/*(seq^\k) is bounded_below by SEQ_2:def 4;
    lim(seq^\k)=x0 by A5,A6,SEQ_4:20;
    then f1/*(seq^\k) is divergent_to+infty by A1,A5,A18;
    then f1/*(seq^\k)+f2/*(seq^\k) is divergent_to+infty by A23,LIMFUNC1:9;
    hence (f1+f2)/*seq is divergent_to+infty by A16,LIMFUNC1:7;
  end;
  hence thesis by A2;
end;

theorem
  f1 is_left_divergent_to+infty_in x0 & (for r st r<x0 ex g st r<g & g<
x0 & g in dom(f1(#)f2)) & (ex r,r1 st 0<r & 0<r1 & for g st g in dom f2 /\ ].x0
  -r,x0.[ holds r1<= f2.g) implies f1(#)f2 is_left_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_left_divergent_to+infty_in x0 and
A2: for r st r<x0 ex g st r<g & g<x0 & g 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.[ holds t<=f2.g;
  now
    let seq such that
A6: seq is convergent and
A7: lim seq=x0 and
A8: rng seq c=dom(f1(#)f2)/\left_open_halfline(x0);
    x0-r<x0 by A3,Lm1;
    then consider k such that
A9: for n st k<=n holds x0-r<seq.n by A6,A7,Th1;
A10: rng seq c=dom(f1(#)f2) by A8,Lm2;
A11: dom(f1(#)f2)=dom f1/\dom f2 by A8,Lm2;
    rng(seq^\k)c=rng seq by VALUED_0:21;
    then
A12: rng(seq^\k)c=dom(f1(#)f2)/\left_open_halfline(x0) by A8,XBOOLE_1:1;
    then
A13: rng(seq^\k)c=dom f2 by Lm2;
A14: rng(seq^\k)c=left_open_halfline(x0) by A12,Lm2;
A15: now
      thus 0<t by A4;
      let n;
A16: n in NAT by ORDINAL1:def 12;
      x0-r<seq.(n+k) by A9,NAT_1:12;
      then
A17:  x0-r<(seq^\k).n by NAT_1:def 3;
A18:  (seq^\k).n in rng(seq^\k) by VALUED_0:28;
      then (seq^\k).n in left_open_halfline(x0) by A14;
      then (seq^\k).n in {g1: g1<x0} by XXREAL_1:229;
      then ex g st g=(seq^\k).n & g<x0;
      then (seq^\k).n in {g2: x0-r<g2 & g2<x0} by A17;
      then (seq^\k).n in ].x0-r,x0.[ by RCOMP_1:def 2;
      then (seq^\k).n in dom f2/\].x0-r,x0.[ by A13,A18,XBOOLE_0:def 4;
      then t<=f2.((seq^\k).n) by A5;
      hence t<=(f2/*(seq^\k)).n by A13,FUNCT_2:108,A16;
    end;
A19: rng(seq^\k)c=dom f1/\left_open_halfline(x0) by A12,Lm2;
    lim(seq^\k)=x0 by A6,A7,SEQ_4:20;
    then f1/*(seq^\k) is divergent_to+infty by A1,A6,A19;
    then
A20: (f1/*(seq^\k))(#)(f2/*(seq^\k)) is divergent_to+infty by A15,LIMFUNC1:22;
    rng(seq^\k)c=dom(f1(#)f2) by A12,Lm2;
    then (f1/*(seq^\k))(#)(f2/*(seq^\k))=(f1(#)f2)/*(seq^\k) by A11,RFUNCT_2:8
      .=((f1(#)f2)/*seq)^\k by A10,VALUED_0:27;
    hence (f1(#)f2)/*seq is divergent_to+infty by A20,LIMFUNC1:7;
  end;
  hence thesis by A2;
end;

theorem
  f1 is_right_divergent_to+infty_in x0 & (for r st x0<r ex g st g<r & x0
<g & g in dom(f1+f2)) & (ex r st 0<r & f2|].x0,x0+r.[ is bounded_below) implies
  f1+f2 is_right_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_right_divergent_to+infty_in x0 and
A2: for r st x0<r ex g st g<r & x0<g & g in dom(f1+f2);
  given r such that
A3: 0<r and
A4: f2|].x0,x0+r.[ is bounded_below;
  now
    let seq such that
A5: seq is convergent and
A6: lim seq=x0 and
A7: rng seq c=dom(f1+f2)/\right_open_halfline(x0);
    x0<x0+r by A3,Lm1;
    then consider k such that
A8: for n st k<=n holds seq.n<x0+r by A5,A6,Th2;
A9: dom(f1+f2)/\right_open_halfline(x0) c=dom(f1+f2) by XBOOLE_1:17;
    rng(seq^\k)c=rng seq by VALUED_0:21;
    then
A10: rng(seq^\k)c=dom(f1+f2)/\right_open_halfline(x0) by A7,XBOOLE_1:1;
    then
A11: rng(seq^\k)c=dom(f1+f2) by A9,XBOOLE_1:1;
A12: dom(f1+f2)=dom f1/\dom f2 by VALUED_1:def 1;
    then
A13: dom(f1+f2)c=dom f2 by XBOOLE_1:17;
    then
A14: rng(seq^\k)c=dom f2 by A11,XBOOLE_1:1;
    dom(f1+f2)c=dom f1 by A12,XBOOLE_1:17;
    then
A15: rng(seq^\k)c=dom f1 by A11,XBOOLE_1:1;
    then rng(seq^\k)c=dom f1/\dom f2 by A14,XBOOLE_1:19;
    then
A16: f1/*(seq^\k)+f2/*(seq^\k)=(f1+f2)/*(seq^\k) by RFUNCT_2:8
      .=((f1+f2)/*seq)^\k by A7,A9,VALUED_0:27,XBOOLE_1:1;
    dom(f1+f2)/\ right_open_halfline(x0) c=right_open_halfline(x0) by
XBOOLE_1:17;
    then
A17: rng(seq^\k)c=right_open_halfline(x0) by A10,XBOOLE_1:1;
    then
A18: rng(seq^\k)c=dom f1/\right_open_halfline(x0) by A15,XBOOLE_1:19;
    now
      consider r1 be Real such that
A19:  for g being object st g in ].x0,x0+r.[/\dom f2 holds r1<=f2.g by A4,
RFUNCT_1:71;
      take r2=r1-1;
      let n;
A20: n in NAT by ORDINAL1:def 12;
      seq.(n+k)<x0+r by A8,NAT_1:12;
      then
A21:  (seq^\k).n<x0+r by NAT_1:def 3;
A22:  (seq^\k).n in rng(seq^\k) by VALUED_0:28;
      then (seq^\k).n in right_open_halfline(x0) by A17;
      then (seq^\k).n in {g1: x0<g1} by XXREAL_1:230;
      then ex g st g=(seq^\k).n & x0<g;
      then (seq^\k).n in {g2: x0<g2 & g2<x0+r} by A21;
      then (seq^\k).n in ].x0,x0+r.[ by RCOMP_1:def 2;
      then (seq^\k).n in ].x0,x0+r.[/\dom f2 by A14,A22,XBOOLE_0:def 4;
      then r1-1<f2.((seq^\k).n)-0 by A19,XREAL_1:15;
      hence r2<(f2/*(seq^\k)).n by A11,A13,FUNCT_2:108,XBOOLE_1:1,A20;
    end;
    then
A23: f2/*(seq^\k) is bounded_below by SEQ_2:def 4;
    lim(seq^\k)=x0 by A5,A6,SEQ_4:20;
    then f1/*(seq^\k) is divergent_to+infty by A1,A5,A18;
    then f1/*(seq^\k)+f2/*(seq^\k) is divergent_to+infty by A23,LIMFUNC1:9;
    hence (f1+f2)/*seq is divergent_to+infty by A16,LIMFUNC1:7;
  end;
  hence thesis by A2;
end;

theorem
  f1 is_right_divergent_to+infty_in x0 & (for r st x0<r ex g st g<r & x0
<g & g in dom(f1(#)f2)) & (ex r,r1 st 0<r & 0<r1 & for g st g in dom f2 /\ ].x0
  ,x0+r.[ holds r1<= f2.g) implies f1(#)f2 is_right_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_right_divergent_to+infty_in x0 and
A2: for r st x0<r ex g st g<r & x0<g & g 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,x0+r.[ holds t<=f2.g;
  now
    let seq such that
A6: seq is convergent and
A7: lim seq=x0 and
A8: rng seq c=dom(f1(#)f2)/\right_open_halfline(x0);
    x0<x0+r by A3,Lm1;
    then consider k such that
A9: for n st k<=n holds seq.n<x0+r by A6,A7,Th2;
A10: rng seq c=dom(f1(#)f2) by A8,Lm2;
A11: dom(f1(#)f2)=dom f1/\dom f2 by A8,Lm2;
    rng(seq^\k)c=rng seq by VALUED_0:21;
    then
A12: rng(seq^\k)c=dom(f1(#)f2)/\right_open_halfline(x0) by A8,XBOOLE_1:1;
    then
A13: rng(seq^\k)c=dom f2 by Lm2;
A14: rng(seq^\k)c=right_open_halfline(x0) by A12,Lm2;
A15: now
      thus 0<t by A4;
      let n;
A16: n in NAT by ORDINAL1:def 12;
      seq.(n+k)<x0+r by A9,NAT_1:12;
      then
A17:  (seq^\k).n<x0+r by NAT_1:def 3;
A18:  (seq^\k).n in rng(seq^\k) by VALUED_0:28;
      then (seq^\k).n in right_open_halfline(x0) by A14;
      then (seq^\k).n in {g1: x0<g1} by XXREAL_1:230;
      then ex g st g=(seq^\k).n & x0<g;
      then (seq^\k).n in {g2: x0<g2 & g2<x0+r} by A17;
      then (seq^\k).n in ].x0,x0+r.[ by RCOMP_1:def 2;
      then (seq^\k).n in dom f2/\].x0,x0+r.[ by A13,A18,XBOOLE_0:def 4;
      then t<=f2.((seq^\k).n) by A5;
      hence t<=(f2/*(seq^\k)).n by A13,FUNCT_2:108,A16;
    end;
A19: rng(seq^\k)c=dom f1/\right_open_halfline(x0) by A12,Lm2;
    lim(seq^\k)=x0 by A6,A7,SEQ_4:20;
    then f1/*(seq^\k) is divergent_to+infty by A1,A6,A19;
    then
A20: (f1/*(seq^\k))(#)(f2/*(seq^\k)) is divergent_to+infty by A15,LIMFUNC1:22;
    rng(seq^\k)c=dom(f1(#)f2) by A12,Lm2;
    then (f1/*(seq^\k))(#)(f2/*(seq^\k))=(f1(#)f2)/*(seq^\k) by A11,RFUNCT_2:8
      .=((f1(#)f2)/*seq)^\k by A10,VALUED_0:27;
    hence (f1(#)f2)/*seq is divergent_to+infty by A20,LIMFUNC1:7;
  end;
  hence thesis by A2;
end;

theorem
  (f is_left_divergent_to+infty_in x0 & r>0 implies r(#)f
is_left_divergent_to+infty_in x0 ) & (f is_left_divergent_to+infty_in x0 & r<0
  implies r(#)f is_left_divergent_to-infty_in x0 ) & (f
  is_left_divergent_to-infty_in x0 & r>0 implies r(#)f
is_left_divergent_to-infty_in x0 ) & (f is_left_divergent_to-infty_in x0 & r<0
  implies r(#)f is_left_divergent_to+infty_in x0 )
proof
A1: dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
  thus f is_left_divergent_to+infty_in x0 & r>0 implies r(#)f
  is_left_divergent_to+infty_in x0
  proof
    assume that
A2: f is_left_divergent_to+infty_in x0 and
A3: r>0;
    thus for r1 st r1<x0 ex g st r1<g & g<x0 & g in dom(r(#)f)
    proof
      let r1;
      assume r1<x0;
      then consider g such that
A4:   r1<g and
A5:   g<x0 and
A6:   g in dom f by A2;
      take g;
      thus thesis by A4,A5,A6,VALUED_1:def 5;
    end;
    let seq;
    assume that
A7: seq is convergent and
A8: lim seq=x0 and
A9: rng seq c=dom(r(#)f)/\left_open_halfline(x0);
A10: dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
A11: rng seq c=dom f/\left_open_halfline(x0) by A9,VALUED_1:def 5;
    then f/*seq is divergent_to+infty by A2,A7,A8;
    then r(#)(f/*seq) is divergent_to+infty by A3,LIMFUNC1:13;
    hence thesis by A11,A10,RFUNCT_2:9,XBOOLE_1:1;
  end;
  thus f is_left_divergent_to+infty_in x0 & r<0 implies r(#)f
  is_left_divergent_to-infty_in x0
  proof
    assume that
A12: f is_left_divergent_to+infty_in x0 and
A13: r<0;
    thus for r1 st r1<x0 ex g st r1<g & g<x0 & g in dom(r(#)f)
    proof
      let r1;
      assume r1<x0;
      then consider g such that
A14:  r1<g and
A15:  g<x0 and
A16:  g in dom f by A12;
      take g;
      thus thesis by A14,A15,A16,VALUED_1:def 5;
    end;
    let seq;
    assume that
A17: seq is convergent and
A18: lim seq=x0 and
A19: rng seq c=dom(r(#)f)/\left_open_halfline(x0);
A20: dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
A21: rng seq c=dom f/\left_open_halfline(x0) by A19,VALUED_1:def 5;
    then f/*seq is divergent_to+infty by A12,A17,A18;
    then r(#)(f/*seq) is divergent_to-infty by A13,LIMFUNC1:13;
    hence thesis by A21,A20,RFUNCT_2:9,XBOOLE_1:1;
  end;
  thus f is_left_divergent_to-infty_in x0 & r>0 implies r(#)f
  is_left_divergent_to-infty_in x0
  proof
    assume that
A22: f is_left_divergent_to-infty_in x0 and
A23: r>0;
    thus for r1 st r1<x0 ex g st r1<g & g<x0 & g in dom(r(#)f)
    proof
      let r1;
      assume r1<x0;
      then consider g such that
A24:  r1<g and
A25:  g<x0 and
A26:  g in dom f by A22;
      take g;
      thus thesis by A24,A25,A26,VALUED_1:def 5;
    end;
    let seq;
    assume that
A27: seq is convergent and
A28: lim seq=x0 and
A29: rng seq c=dom(r(#)f)/\left_open_halfline(x0);
A30: dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
A31: rng seq c=dom f/\left_open_halfline(x0) by A29,VALUED_1:def 5;
    then f/*seq is divergent_to-infty by A22,A27,A28;
    then r(#)(f/*seq) is divergent_to-infty by A23,LIMFUNC1:14;
    hence thesis by A31,A30,RFUNCT_2:9,XBOOLE_1:1;
  end;
  assume that
A32: f is_left_divergent_to-infty_in x0 and
A33: r<0;
  thus for r1 st r1<x0 ex g st r1<g & g<x0 & g in dom(r(#)f)
  proof
    let r1;
    assume r1<x0;
    then consider g such that
A34: r1<g and
A35: g<x0 and
A36: g in dom f by A32;
    take g;
    thus thesis by A34,A35,A36,VALUED_1:def 5;
  end;
  let seq;
  assume that
A37: seq is convergent and
A38: lim seq=x0 and
A39: rng seq c=dom(r(#)f)/\left_open_halfline(x0);
A40: rng seq c=dom f/\left_open_halfline(x0) by A39,VALUED_1:def 5;
  then f/*seq is divergent_to-infty by A32,A37,A38;
  then r(#)(f/*seq) is divergent_to+infty by A33,LIMFUNC1:14;
  hence thesis by A40,A1,RFUNCT_2:9,XBOOLE_1:1;
end;

theorem
  (f is_right_divergent_to+infty_in x0 & r>0 implies r(#)f
is_right_divergent_to+infty_in x0 ) & (f is_right_divergent_to+infty_in x0 & r<
  0 implies r(#)f is_right_divergent_to-infty_in x0 ) & (f
  is_right_divergent_to-infty_in x0 & r>0 implies r(#)f
is_right_divergent_to-infty_in x0 ) & (f is_right_divergent_to-infty_in x0 & r<
  0 implies r(#)f is_right_divergent_to+infty_in x0)
proof
A1: dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
  thus f is_right_divergent_to+infty_in x0 & r>0 implies r(#)f
  is_right_divergent_to+infty_in x0
  proof
    assume that
A2: f is_right_divergent_to+infty_in x0 and
A3: r>0;
    thus for r1 st x0<r1 ex g st g<r1 & x0<g & g in dom(r(#)f)
    proof
      let r1;
      assume x0<r1;
      then consider g such that
A4:   g<r1 and
A5:   x0<g and
A6:   g in dom f by A2;
      take g;
      thus thesis by A4,A5,A6,VALUED_1:def 5;
    end;
    let seq;
    assume that
A7: seq is convergent and
A8: lim seq=x0 and
A9: rng seq c=dom(r(#)f)/\right_open_halfline(x0);
A10: dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
A11: rng seq c=dom f/\right_open_halfline(x0) by A9,VALUED_1:def 5;
    then f/*seq is divergent_to+infty by A2,A7,A8;
    then r(#)(f/*seq) is divergent_to+infty by A3,LIMFUNC1:13;
    hence thesis by A11,A10,RFUNCT_2:9,XBOOLE_1:1;
  end;
  thus f is_right_divergent_to+infty_in x0 & r<0 implies r(#)f
  is_right_divergent_to-infty_in x0
  proof
    assume that
A12: f is_right_divergent_to+infty_in x0 and
A13: r<0;
    thus for r1 st x0<r1 ex g st g<r1 & x0<g & g in dom(r(#)f)
    proof
      let r1;
      assume x0<r1;
      then consider g such that
A14:  g<r1 and
A15:  x0<g and
A16:  g in dom f by A12;
      take g;
      thus thesis by A14,A15,A16,VALUED_1:def 5;
    end;
    let seq;
    assume that
A17: seq is convergent and
A18: lim seq=x0 and
A19: rng seq c=dom(r(#)f)/\right_open_halfline(x0);
A20: dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
A21: rng seq c=dom f/\right_open_halfline(x0) by A19,VALUED_1:def 5;
    then f/*seq is divergent_to+infty by A12,A17,A18;
    then r(#)(f/*seq) is divergent_to-infty by A13,LIMFUNC1:13;
    hence thesis by A21,A20,RFUNCT_2:9,XBOOLE_1:1;
  end;
  thus f is_right_divergent_to-infty_in x0 & r>0 implies r(#)f
  is_right_divergent_to-infty_in x0
  proof
    assume that
A22: f is_right_divergent_to-infty_in x0 and
A23: r>0;
    thus for r1 st x0<r1 ex g st g<r1 & x0<g & g in dom(r(#)f)
    proof
      let r1;
      assume x0<r1;
      then consider g such that
A24:  g<r1 and
A25:  x0<g and
A26:  g in dom f by A22;
      take g;
      thus thesis by A24,A25,A26,VALUED_1:def 5;
    end;
    let seq;
    assume that
A27: seq is convergent and
A28: lim seq=x0 and
A29: rng seq c=dom(r(#)f)/\right_open_halfline(x0);
A30: dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
A31: rng seq c=dom f/\right_open_halfline(x0) by A29,VALUED_1:def 5;
    then f/*seq is divergent_to-infty by A22,A27,A28;
    then r(#)(f/*seq) is divergent_to-infty by A23,LIMFUNC1:14;
    hence thesis by A31,A30,RFUNCT_2:9,XBOOLE_1:1;
  end;
  assume that
A32: f is_right_divergent_to-infty_in x0 and
A33: r<0;
  thus for r1 st x0<r1 ex g st g<r1 & x0<g & g in dom(r(#)f)
  proof
    let r1;
    assume x0<r1;
    then consider g such that
A34: g<r1 and
A35: x0<g and
A36: g in dom f by A32;
    take g;
    thus thesis by A34,A35,A36,VALUED_1:def 5;
  end;
  let seq;
  assume that
A37: seq is convergent and
A38: lim seq=x0 and
A39: rng seq c=dom(r(#)f)/\right_open_halfline(x0);
A40: rng seq c=dom f/\right_open_halfline(x0) by A39,VALUED_1:def 5;
  then f/*seq is divergent_to-infty by A32,A37,A38;
  then r(#)(f/*seq) is divergent_to+infty by A33,LIMFUNC1:14;
  hence thesis by A40,A1,RFUNCT_2:9,XBOOLE_1:1;
end;

theorem
  (f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in
  x0) implies abs(f) is_left_divergent_to+infty_in x0
proof
  assume
A1: f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0;
  now
    per cases by A1;
    suppose
A2:   f is_left_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)/\left_open_halfline(x0);
A7:     rng seq c=dom f/\left_open_halfline(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;
        dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
        then 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 r;
        assume r<x0;
        then consider g such that
A9:     r<g and
A10:    g<x0 and
A11:    g in dom f by A2;
        take g;
        thus r<g & g<x0 & g in dom abs(f) by A9,A10,A11,VALUED_1:def 11;
      end;
      hence thesis by A3;
    end;
    suppose
A12:  f is_left_divergent_to-infty_in x0;
A13:  now
        let seq;
        assume that
A14:    seq is convergent and
A15:    lim seq=x0 and
A16:    rng seq c=dom abs(f)/\left_open_halfline(x0);
A17:    rng seq c=dom f/\left_open_halfline(x0) by A16,VALUED_1:def 11;
        then f/*seq is divergent_to-infty by A12,A14,A15;
        then
A18:    abs(f/*seq) is divergent_to+infty by LIMFUNC1:25;
        dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
        then rng seq c=dom f by A17,XBOOLE_1:1;
        hence (abs f)/*seq is divergent_to+infty by A18,RFUNCT_2:10;
      end;
      now
        let r;
        assume r<x0;
        then consider g such that
A19:    r<g and
A20:    g<x0 and
A21:    g in dom f by A12;
        take g;
        thus r<g & g<x0 & g in dom abs(f) by A19,A20,A21,VALUED_1:def 11;
      end;
      hence thesis by A13;
    end;
  end;
  hence thesis;
end;

theorem
  (f is_right_divergent_to+infty_in x0 or f
  is_right_divergent_to-infty_in x0 ) implies abs(f)
  is_right_divergent_to+infty_in x0
proof
  assume
A1: f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0;
  now
    per cases by A1;
    suppose
A2:   f is_right_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)/\right_open_halfline(x0);
A7:     rng seq c=dom f/\right_open_halfline(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;
        dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
        then 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 r;
        assume x0<r;
        then consider g such that
A9:     g<r and
A10:    x0<g and
A11:    g in dom f by A2;
        take g;
        thus g<r & x0<g & g in dom abs(f) by A9,A10,A11,VALUED_1:def 11;
      end;
      hence thesis by A3;
    end;
    suppose
A12:  f is_right_divergent_to-infty_in x0;
A13:  now
        let seq;
        assume that
A14:    seq is convergent and
A15:    lim seq=x0 and
A16:    rng seq c=dom abs(f)/\right_open_halfline(x0);
A17:    rng seq c=dom f/\right_open_halfline(x0) by A16,VALUED_1:def 11;
        then f/*seq is divergent_to-infty by A12,A14,A15;
        then
A18:    abs(f/*seq) is divergent_to+infty by LIMFUNC1:25;
        dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
        then rng seq c=dom f by A17,XBOOLE_1:1;
        hence (abs f)/*seq is divergent_to+infty by A18,RFUNCT_2:10;
      end;
      now
        let r;
        assume x0<r;
        then consider g such that
A19:    g<r and
A20:    x0<g and
A21:    g in dom f by A12;
        take g;
        thus g<r & x0<g & g in dom abs(f) by A19,A20,A21,VALUED_1:def 11;
      end;
      hence thesis by A13;
    end;
  end;
  hence thesis;
end;

theorem Th25:
  (ex r st f|].x0-r,x0.[ is non-decreasing& not f|].x0-r,x0.[ is
  bounded_above) & (for r st r<x0 ex g st r<g & g<x0 & g in dom f) implies f
  is_left_divergent_to+infty_in x0
proof
  given r such that
A1: f|].x0-r,x0.[ is non-decreasing and
A2: not f|].x0-r,x0.[ is bounded_above;
  assume for r st r<x0 ex g st r<g & g<x0 & g in dom f;
  hence for r st r<x0 ex g st r<g & g<x0 & g in dom f;
  let seq such that
A3: seq is convergent and
A4: lim seq=x0 and
A5: rng seq c=dom f/\left_open_halfline(x0);
  now
    let t;
A6: dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
    consider g1 being object such that
A7: g1 in ].x0-r,x0.[/\dom f and
A8: t<f.g1 by A2,RFUNCT_1:70;
    reconsider g1 as Real by A7;
    g1 in ].x0-r,x0.[ by A7,XBOOLE_0:def 4;
    then g1 in {r1: x0-r<r1 & r1<x0} by RCOMP_1:def 2;
    then
A9: ex r1 st r1=g1 & x0-r<r1 & r1<x0;
    then consider n such that
A10: for k st n<=k holds g1<seq.k by A3,A4,Th1;
    take n;
    let k;
A11: k in NAT by ORDINAL1:def 12;
    seq.k in rng seq by VALUED_0:28;
    then
A12: seq.k in dom f/\left_open_halfline(x0) by A5;
    dom f/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
    then seq.k in left_open_halfline(x0) by A12;
    then seq.k in {r2: r2<x0} by XXREAL_1:229;
    then
A13: ex r2 st r2=seq.k & r2<x0;
    assume n<=k;
    then
A14: g1<seq.k by A10;
    then x0-r<seq.k by A9,XXREAL_0:2;
    then seq.k in {g2: x0-r<g2 & g2<x0} by A13;
    then seq.k in ].x0-r,x0.[ by RCOMP_1:def 2;
    then seq.k in ].x0-r,x0.[/\dom f by A12,A6,XBOOLE_0:def 4;
    then f.g1<=f.(seq.k) by A1,A7,A14,RFUNCT_2:22;
    then t<f.(seq.k) by A8,XXREAL_0:2;
    hence t<(f/*seq).k by A5,A6,FUNCT_2:108,XBOOLE_1:1,A11;
  end;
  hence thesis;
end;

theorem
  (ex r st 0<r & f|].x0-r,x0.[ is increasing & not f|].x0-r,x0.[ is
  bounded_above) & (for r st r<x0 ex g st r<g & g<x0 & g in dom f) implies f
  is_left_divergent_to+infty_in x0 by Th25;

theorem Th27:
  (ex r st f|].x0-r,x0.[ is non-increasing & not f|].x0-r,x0.[ is
  bounded_below) & (for r st r<x0 ex g st r<g & g<x0 & g in dom f) implies f
  is_left_divergent_to-infty_in x0
proof
  given r such that
A1: f|].x0-r,x0.[ is non-increasing and
A2: not f|].x0-r,x0.[ is bounded_below;
  assume for r st r<x0 ex g st r<g & g<x0 & g in dom f;
  hence for r st r<x0 ex g st r<g & g<x0 & g in dom f;
  let seq such that
A3: seq is convergent and
A4: lim seq=x0 and
A5: rng seq c=dom f/\left_open_halfline(x0);
  now
    let t;
A6: dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
    consider g1 being object such that
A7: g1 in ].x0-r,x0.[/\dom f and
A8: f.g1<t by A2,RFUNCT_1:71;
    reconsider g1 as Real by A7;
    g1 in ].x0-r,x0.[ by A7,XBOOLE_0:def 4;
    then g1 in {r1: x0-r<r1 & r1<x0} by RCOMP_1:def 2;
    then
A9: ex r1 st r1=g1 & x0-r<r1 & r1<x0;
    then consider n such that
A10: for k st n<=k holds g1<seq.k by A3,A4,Th1;
    take n;
    let k;
A11: k in NAT by ORDINAL1:def 12;
    seq.k in rng seq by VALUED_0:28;
    then
A12: seq.k in dom f/\left_open_halfline(x0) by A5;
    dom f/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
    then seq.k in left_open_halfline(x0) by A12;
    then seq.k in {r2: r2<x0} by XXREAL_1:229;
    then
A13: ex r2 st r2=seq.k & r2<x0;
    assume n<=k;
    then
A14: g1<seq.k by A10;
    then x0-r<seq.k by A9,XXREAL_0:2;
    then seq.k in {g2: x0-r<g2 & g2<x0} by A13;
    then seq.k in ].x0-r,x0.[ by RCOMP_1:def 2;
    then seq.k in ].x0-r,x0.[/\dom f by A12,A6,XBOOLE_0:def 4;
    then f.(seq.k)<=f.g1 by A1,A7,A14,RFUNCT_2:23;
    then f.(seq.k)<t by A8,XXREAL_0:2;
    hence (f/*seq).k<t by A5,A6,FUNCT_2:108,XBOOLE_1:1,A11;
  end;
  hence thesis;
end;

theorem
  (ex r st 0<r & f|].x0-r,x0.[ is decreasing & not f|].x0-r,x0.[ is
  bounded_below) & (for r st r<x0 ex g st r<g & g<x0 & g in dom f) implies f
  is_left_divergent_to-infty_in x0 by Th27;

theorem Th29:
  (ex r st f|].x0,x0+r.[ is non-increasing & not f|].x0,x0+r.[ is
  bounded_above) & (for r st x0<r ex g st g<r & x0<g & g in dom f) implies f
  is_right_divergent_to+infty_in x0
proof
  given r such that
A1: f|].x0,x0+r.[ is non-increasing and
A2: not f|].x0,x0+r.[ is bounded_above;
  assume for r st x0<r ex g st g<r & x0<g & g in dom f;
  hence for r st x0<r ex g st g<r & x0<g & g in dom f;
  let seq such that
A3: seq is convergent and
A4: lim seq=x0 and
A5: rng seq c=dom f/\right_open_halfline(x0);
  now
    let t;
A6: dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
    consider g1 being object such that
A7: g1 in ].x0,x0+r.[/\dom f and
A8: t<f.g1 by A2,RFUNCT_1:70;
    reconsider g1 as Real by A7;
    g1 in ].x0,x0+r.[ by A7,XBOOLE_0:def 4;
    then g1 in {r1: x0<r1 & r1<x0+r} by RCOMP_1:def 2;
    then
A9: ex r1 st r1=g1 & x0<r1 & r1<x0+r;
    then consider n such that
A10: for k st n<=k holds seq.k<g1 by A3,A4,Th2;
    take n;
    let k;
    seq.k in rng seq by VALUED_0:28;
    then
A11: seq.k in dom f/\right_open_halfline(x0) by A5;
    dom f/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
    then seq.k in right_open_halfline(x0) by A11;
    then seq.k in {r2: x0<r2} by XXREAL_1:230;
    then
A12: ex r2 st r2=seq.k & x0<r2;
A13: k in NAT by ORDINAL1:def 12;
    assume n<=k;
    then
A14: seq.k<g1 by A10;
    then seq.k<x0+r by A9,XXREAL_0:2;
    then seq.k in {g2: x0<g2 & g2<x0+r} by A12;
    then seq.k in ].x0,x0+r.[ by RCOMP_1:def 2;
    then seq.k in ].x0,x0+r.[/\dom f by A11,A6,XBOOLE_0:def 4;
    then f.g1<=f.(seq.k) by A1,A7,A14,RFUNCT_2:23;
    then t<f.(seq.k) by A8,XXREAL_0:2;
    hence t<(f/*seq).k by A5,A6,FUNCT_2:108,XBOOLE_1:1,A13;
  end;
  hence thesis;
end;

theorem
  (ex r st 0<r & f|].x0,x0+r.[ is decreasing & not f|].x0,x0+r.[ is
  bounded_above) & (for r st x0<r ex g st g<r & x0<g & g in dom f) implies f
  is_right_divergent_to+infty_in x0 by Th29;

theorem Th31:
  (ex r st f|].x0,x0+r.[ is non-decreasing & not f|].x0,x0+r.[ is
  bounded_below) & (for r st x0<r ex g st g<r & x0<g & g in dom f) implies f
  is_right_divergent_to-infty_in x0
proof
  given r such that
A1: f|].x0,x0+r.[ is non-decreasing and
A2: not f|].x0,x0+r.[ is bounded_below;
  assume for r st x0<r ex g st g<r & x0<g & g in dom f;
  hence for r st x0<r ex g st g<r & x0<g & g in dom f;
  let seq such that
A3: seq is convergent and
A4: lim seq=x0 and
A5: rng seq c=dom f/\right_open_halfline(x0);
  now
    let t;
A6: dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
    consider g1 being object such that
A7: g1 in ].x0,x0+r.[/\dom f and
A8: f.g1<t by A2,RFUNCT_1:71;
    reconsider g1 as Real by A7;
    g1 in ].x0,x0+r.[ by A7,XBOOLE_0:def 4;
    then g1 in {r1: x0<r1 & r1<x0+r} by RCOMP_1:def 2;
    then
A9: ex r1 st r1=g1 & x0<r1 & r1<x0+r;
    then consider n such that
A10: for k st n<=k holds seq.k<g1 by A3,A4,Th2;
    take n;
    let k;
    seq.k in rng seq by VALUED_0:28;
    then
A11: seq.k in dom f/\right_open_halfline(x0) by A5;
    dom f/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
    then seq.k in right_open_halfline(x0) by A11;
    then seq.k in {r2: x0<r2} by XXREAL_1:230;
    then
A12: ex r2 st r2=seq.k & x0<r2;
A13: k in NAT by ORDINAL1:def 12;
    assume n<=k;
    then
A14: seq.k<g1 by A10;
    then seq.k<x0+r by A9,XXREAL_0:2;
    then seq.k in {g2: x0<g2 & g2<x0+r} by A12;
    then seq.k in ].x0,x0+r.[ by RCOMP_1:def 2;
    then seq.k in ].x0,x0+r.[/\dom f by A11,A6,XBOOLE_0:def 4;
    then f.(seq.k)<=f.g1 by A1,A7,A14,RFUNCT_2:22;
    then f.(seq.k)<t by A8,XXREAL_0:2;
    hence (f/*seq).k<t by A5,A6,FUNCT_2:108,XBOOLE_1:1,A13;
  end;
  hence thesis;
end;

theorem
  (ex r st 0<r & f|].x0,x0+r.[ is increasing & not f|].x0,x0+r.[ is
  bounded_below) & (for r st x0<r ex g st g<r & x0<g & g in dom f) implies f
  is_right_divergent_to-infty_in x0 by Th31;

theorem Th33:
  f1 is_left_divergent_to+infty_in x0 & (for r st r<x0 ex g st r<g
& g<x0 & g in dom f) & (ex r st 0<r & dom f /\ ].x0-r,x0.[ c= dom f1 /\ ].x0-r,
  x0.[ & for g st g in dom f /\ ].x0-r,x0.[ holds f1.g<=f.g) implies f
  is_left_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_left_divergent_to+infty_in x0 and
A2: for r st r<x0 ex g st r<g & g<x0 & g in dom f;
  given r such that
A3: 0<r and
A4: dom f/\].x0-r,x0.[c=dom f1/\].x0-r,x0.[ and
A5: for g st g in dom f/\].x0-r,x0.[ holds f1.g<=f.g;
  thus for r st r<x0 ex g st r<g & g<x0 & g in dom f by A2;
  let seq such that
A6: seq is convergent and
A7: lim seq=x0 and
A8: rng seq c=dom f/\left_open_halfline(x0);
  x0-r<x0 by A3,Lm1;
  then consider k such that
A9: for n st k<=n holds x0-r<seq.n by A6,A7,Th1;
A10: rng(seq^\k)c= rng seq by VALUED_0:21;
  dom f/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
  then rng seq c=left_open_halfline(x0) by A8,XBOOLE_1:1;
  then
A11: rng(seq^\k)c=left_open_halfline(x0) by A10,XBOOLE_1:1;
  now
    let x be object;
    assume
A12: x in rng(seq^\k);
    then consider n being Element of NAT such that
A13: (seq^\k).n=x by FUNCT_2:113;
    (seq^\k).n in left_open_halfline(x0) by A11,A12,A13;
    then (seq^\k).n in {g: g<x0} by XXREAL_1:229;
    then
A14: ex r1 st r1=(seq^\k).n & r1<x0;
    x0-r<seq.(n+k) by A9,NAT_1:12;
    then x0-r<(seq^\k).n by NAT_1:def 3;
    then x in {g1: x0-r<g1 & g1<x0} by A13,A14;
    hence x in ].x0-r,x0.[ by RCOMP_1:def 2;
  end;
  then
A15: rng(seq^\k)c=].x0-r,x0.[ by TARSKI:def 3;
A16: dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
  then
A17: rng seq c=dom f by A8,XBOOLE_1:1;
  then rng(seq^\k)c=dom f by A10,XBOOLE_1:1;
  then
A18: rng(seq^\k)c=dom f/\].x0-r,x0.[ by A15,XBOOLE_1:19;
  then
A19: rng(seq^\k)c=dom f1/\].x0-r,x0.[ by A4,XBOOLE_1:1;
A20: dom f1/\].x0-r,x0.[c=dom f1 by XBOOLE_1:17;
  then rng(seq^\k)c=dom f1 by A19,XBOOLE_1:1;
  then
A21: rng(seq^\k)c=dom f1/\left_open_halfline(x0) by A11,XBOOLE_1:19;
A22: now
    let n;
A23: n in NAT by ORDINAL1:def 12;
    (seq^\k).n in rng(seq^\k) by VALUED_0:28;
    then f1.((seq^\k).n)<=f.((seq^\k).n) by A5,A18;
    then (f1/*(seq^\k)).n<=f.((seq^\k).n)
          by A19,A20,FUNCT_2:108,XBOOLE_1:1,A23;
    hence (f1/*(seq^\k)).n<=(f/*(seq^\k)).n
by A17,A10,FUNCT_2:108,XBOOLE_1:1,A23;
  end;
  lim(seq^\k)=x0 by A6,A7,SEQ_4:20;
  then f1/*(seq^\k) is divergent_to+infty by A1,A6,A21;
  then f/*(seq^\k) is divergent_to+infty by A22,LIMFUNC1:42;
  then (f/*seq)^\k is divergent_to+infty by A8,A16,VALUED_0:27,XBOOLE_1:1;
  hence thesis by LIMFUNC1:7;
end;

theorem Th34:
  f1 is_left_divergent_to-infty_in x0 & (for r st r<x0 ex g st r<g
& g<x0 & g in dom f) & (ex r st 0<r & dom f /\ ].x0-r,x0.[ c= dom f1 /\ ].x0-r,
  x0.[ & for g st g in dom f /\ ].x0-r,x0.[ holds f.g<=f1.g) implies f
  is_left_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_left_divergent_to-infty_in x0 and
A2: for r st r<x0 ex g st r<g & g<x0 & g in dom f;
  given r such that
A3: 0<r and
A4: dom f/\].x0-r,x0.[c=dom f1/\].x0-r,x0.[ and
A5: for g st g in dom f/\].x0-r,x0.[ holds f.g<=f1.g;
  thus for r st r<x0 ex g st r<g & g<x0 & g in dom f by A2;
  let seq such that
A6: seq is convergent and
A7: lim seq=x0 and
A8: rng seq c=dom f/\left_open_halfline(x0);
  x0-r<x0 by A3,Lm1;
  then consider k such that
A9: for n st k<=n holds x0-r<seq.n by A6,A7,Th1;
A10: rng(seq^\k)c= rng seq by VALUED_0:21;
  dom f/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
  then rng seq c=left_open_halfline(x0) by A8,XBOOLE_1:1;
  then
A11: rng(seq^\k)c=left_open_halfline(x0) by A10,XBOOLE_1:1;
  now
    let x be object;
    assume
A12: x in rng(seq^\k);
    then consider n being Element of NAT such that
A13: (seq^\k).n=x by FUNCT_2:113;
    (seq^\k).n in left_open_halfline(x0) by A11,A12,A13;
    then (seq^\k).n in {g: g<x0} by XXREAL_1:229;
    then
A14: ex r1 st r1=(seq^\k).n & r1<x0;
    x0-r<seq.(n+k) by A9,NAT_1:12;
    then x0-r<(seq^\k).n by NAT_1:def 3;
    then x in {g1: x0-r<g1 & g1<x0} by A13,A14;
    hence x in ].x0-r,x0.[ by RCOMP_1:def 2;
  end;
  then
A15: rng(seq^\k)c=].x0-r,x0.[ by TARSKI:def 3;
A16: dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
  then
A17: rng seq c=dom f by A8,XBOOLE_1:1;
  then rng(seq^\k)c=dom f by A10,XBOOLE_1:1;
  then
A18: rng(seq^\k)c=dom f/\].x0-r,x0.[ by A15,XBOOLE_1:19;
  then
A19: rng(seq^\k)c=dom f1/\].x0-r,x0.[ by A4,XBOOLE_1:1;
A20: dom f1/\].x0-r,x0.[c=dom f1 by XBOOLE_1:17;
  then rng(seq^\k)c=dom f1 by A19,XBOOLE_1:1;
  then
A21: rng(seq^\k)c=dom f1/\left_open_halfline(x0) by A11,XBOOLE_1:19;
A22: now
    let n;
A23: n in NAT by ORDINAL1:def 12;
    (seq^\k).n in rng(seq^\k) by VALUED_0:28;
    then f.((seq^\k).n)<=f1.((seq^\k).n) by A5,A18;
    then (f/*(seq^\k)).n<=f1.((seq^\k).n)
by A17,A10,FUNCT_2:108,XBOOLE_1:1,A23;
    hence (f/*(seq^\k)).n<=(f1/*(seq^\k)).n
by A19,A20,FUNCT_2:108,XBOOLE_1:1,A23;
  end;
  lim(seq^\k)=x0 by A6,A7,SEQ_4:20;
  then f1/*(seq^\k) is divergent_to-infty by A1,A6,A21;
  then f/*(seq^\k) is divergent_to-infty by A22,LIMFUNC1:43;
  then (f/*seq)^\k is divergent_to-infty by A8,A16,VALUED_0:27,XBOOLE_1:1;
  hence thesis by LIMFUNC1:7;
end;

theorem Th35:
  f1 is_right_divergent_to+infty_in x0 & (for r st x0<r ex g st g<
r & x0<g & g in dom f) & (ex r st 0<r & dom f /\ ].x0,x0+r.[ c= dom f1 /\ ].x0,
  x0+r.[ & for g st g in dom f /\ ].x0,x0+r.[ holds f1.g<=f.g) implies f
  is_right_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_right_divergent_to+infty_in x0 and
A2: for r st x0<r ex g st g<r & x0<g & g in dom f;
  given r such that
A3: 0<r and
A4: dom f/\].x0,x0+r.[c=dom f1/\].x0,x0+r.[ and
A5: for g st g in dom f/\].x0,x0+r.[ holds f1.g<=f.g;
  thus for r st x0<r ex g st g<r & x0<g & g in dom f by A2;
  let seq such that
A6: seq is convergent and
A7: lim seq=x0 and
A8: rng seq c=dom f/\right_open_halfline(x0);
  x0<x0+r by A3,Lm1;
  then consider k such that
A9: for n st k<=n holds seq.n<x0+r by A6,A7,Th2;
A10: rng(seq^\k)c= rng seq by VALUED_0:21;
  dom f/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
  then rng seq c=right_open_halfline(x0) by A8,XBOOLE_1:1;
  then
A11: rng(seq^\k)c=right_open_halfline(x0) by A10,XBOOLE_1:1;
  now
    let x be object;
    assume
A12: x in rng(seq^\k);
    then consider n being Element of NAT such that
A13: (seq^\k).n=x by FUNCT_2:113;
    (seq^\k).n in right_open_halfline(x0) by A11,A12,A13;
    then (seq^\k).n in {g: x0<g} by XXREAL_1:230;
    then
A14: ex r1 st r1=(seq^\k).n & x0<r1;
    seq.(n+k)<x0+r by A9,NAT_1:12;
    then (seq^\k).n<x0+r by NAT_1:def 3;
    then x in {g1: x0<g1 & g1<x0+r} by A13,A14;
    hence x in ].x0,x0+r.[ by RCOMP_1:def 2;
  end;
  then
A15: rng(seq^\k)c=].x0,x0+r.[ by TARSKI:def 3;
A16: dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
  then
A17: rng seq c=dom f by A8,XBOOLE_1:1;
  then rng(seq^\k)c=dom f by A10,XBOOLE_1:1;
  then
A18: rng(seq^\k)c=dom f/\].x0,x0+r.[ by A15,XBOOLE_1:19;
  then
A19: rng(seq^\k)c=dom f1/\].x0,x0+r.[ by A4,XBOOLE_1:1;
A20: dom f1/\].x0,x0+r.[c=dom f1 by XBOOLE_1:17;
  then rng(seq^\k)c=dom f1 by A19,XBOOLE_1:1;
  then
A21: rng(seq^\k)c=dom f1/\right_open_halfline(x0) by A11,XBOOLE_1:19;
A22: now
    let n;
A23: n in NAT by ORDINAL1:def 12;
    (seq^\k).n in rng(seq^\k) by VALUED_0:28;
    then f1.((seq^\k).n)<=f.((seq^\k).n) by A5,A18;
    then (f1/*(seq^\k)).n<=f.((seq^\k).n)
by A19,A20,FUNCT_2:108,XBOOLE_1:1,A23;
    hence (f1/*(seq^\k)).n<=(f/*(seq^\k)).n
by A17,A10,FUNCT_2:108,XBOOLE_1:1,A23;
  end;
  lim(seq^\k)=x0 by A6,A7,SEQ_4:20;
  then f1/*(seq^\k) is divergent_to+infty by A1,A6,A21;
  then f/*(seq^\k) is divergent_to+infty by A22,LIMFUNC1:42;
  then (f/*seq)^\k is divergent_to+infty by A8,A16,VALUED_0:27,XBOOLE_1:1;
  hence thesis by LIMFUNC1:7;
end;

theorem Th36:
  f1 is_right_divergent_to-infty_in x0 & (for r st x0<r ex g st g<
r & x0<g & g in dom f) & (ex r st 0<r & dom f /\ ].x0,x0+r.[ c= dom f1 /\ ].x0,
  x0+r.[ & for g st g in dom f /\ ].x0,x0+r.[ holds f.g<=f1.g) implies f
  is_right_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_right_divergent_to-infty_in x0 and
A2: for r st x0<r ex g st g<r & x0<g & g in dom f;
  given r such that
A3: 0<r and
A4: dom f/\].x0,x0+r.[c=dom f1/\].x0,x0+r.[ and
A5: for g st g in dom f/\].x0,x0+r.[ holds f.g<=f1.g;
  thus for r st x0<r ex g st g<r & x0<g & g in dom f by A2;
  let seq such that
A6: seq is convergent and
A7: lim seq=x0 and
A8: rng seq c=dom f/\right_open_halfline(x0);
  x0<x0+r by A3,Lm1;
  then consider k such that
A9: for n st k<=n holds seq.n<x0+r by A6,A7,Th2;
A10: rng(seq^\k)c= rng seq by VALUED_0:21;
  dom f/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
  then rng seq c=right_open_halfline(x0) by A8,XBOOLE_1:1;
  then
A11: rng(seq^\k)c=right_open_halfline(x0) by A10,XBOOLE_1:1;
  now
    let x be object;
    assume
A12: x in rng(seq^\k);
    then consider n being Element of NAT such that
A13: (seq^\k).n=x by FUNCT_2:113;
    (seq^\k).n in right_open_halfline(x0) by A11,A12,A13;
    then (seq^\k).n in {g: x0<g} by XXREAL_1:230;
    then
A14: ex r1 st r1=(seq^\k).n & x0<r1;
    seq.(n+k)<x0+r by A9,NAT_1:12;
    then (seq^\k).n<x0+r by NAT_1:def 3;
    then x in {g1: x0<g1 & g1<x0+r} by A13,A14;
    hence x in ].x0,x0+r.[ by RCOMP_1:def 2;
  end;
  then
A15: rng(seq^\k)c=].x0,x0+r.[ by TARSKI:def 3;
A16: dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
  then
A17: rng seq c=dom f by A8,XBOOLE_1:1;
  then rng(seq^\k)c=dom f by A10,XBOOLE_1:1;
  then
A18: rng(seq^\k)c=dom f/\].x0,x0+r.[ by A15,XBOOLE_1:19;
  then
A19: rng(seq^\k)c=dom f1/\].x0,x0+r.[ by A4,XBOOLE_1:1;
A20: dom f1/\].x0,x0+r.[c=dom f1 by XBOOLE_1:17;
  then rng(seq^\k)c=dom f1 by A19,XBOOLE_1:1;
  then
A21: rng(seq^\k)c=dom f1/\right_open_halfline(x0) by A11,XBOOLE_1:19;
A22: now
    let n;
A23: n in NAT by ORDINAL1:def 12;
    (seq^\k).n in rng(seq^\k) by VALUED_0:28;
    then f.((seq^\k).n)<=f1.((seq^\k).n) by A5,A18;
    then (f/*(seq^\k)).n<=f1.((seq^\k).n)
by A17,A10,FUNCT_2:108,XBOOLE_1:1,A23;
    hence (f/*(seq^\k)).n<=(f1/*(seq^\k)).n
by A19,A20,FUNCT_2:108,XBOOLE_1:1,A23;
  end;
  lim(seq^\k)=x0 by A6,A7,SEQ_4:20;
  then f1/*(seq^\k) is divergent_to-infty by A1,A6,A21;
  then f/*(seq^\k) is divergent_to-infty by A22,LIMFUNC1:43;
  then (f/*seq)^\k is divergent_to-infty by A8,A16,VALUED_0:27,XBOOLE_1:1;
  hence thesis by LIMFUNC1:7;
end;

theorem
  f1 is_left_divergent_to+infty_in x0 & (ex r st 0<r & ].x0-r,x0.[ c=
  dom f /\ dom f1 & for g st g in ].x0-r,x0.[ holds f1.g<= f.g) implies f
  is_left_divergent_to+infty_in x0
proof
  assume
A1: f1 is_left_divergent_to+infty_in x0;
  given r such that
A2: 0<r and
A3: ].x0-r,x0.[ c=dom f/\dom f1 and
A4: for g st g in ].x0-r,x0.[ holds f1.g<=f.g;
A5: dom f/\dom f1 c=dom f by XBOOLE_1:17;
  then
A6: ].x0-r,x0.[=dom f/\].x0-r,x0.[ by A3,XBOOLE_1:1,28;
  dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
  then
A7: ].x0-r,x0.[=dom f1/\].x0-r,x0.[ by A3,XBOOLE_1:1,28;
  for r st r<x0 ex g st r<g & g<x0 & g in dom f by A2,A3,A5,Th3,XBOOLE_1:1;
  hence thesis by A1,A2,A4,A6,A7,Th33;
end;

theorem
  f1 is_left_divergent_to-infty_in x0 & (ex r st 0<r & ].x0-r,x0.[ c=
  dom f /\ dom f1 & for g st g in ].x0-r,x0.[ holds f.g<= f1.g) implies f
  is_left_divergent_to-infty_in x0
proof
  assume
A1: f1 is_left_divergent_to-infty_in x0;
  given r such that
A2: 0<r and
A3: ].x0-r,x0.[c=dom f/\dom f1 and
A4: for g st g in ].x0-r,x0.[ holds f.g<=f1.g;
A5: dom f/\dom f1 c=dom f by XBOOLE_1:17;
  then
A6: ].x0-r,x0.[=dom f/\].x0-r,x0.[ by A3,XBOOLE_1:1,28;
  dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
  then
A7: ].x0-r,x0.[=dom f1/\].x0-r,x0.[ by A3,XBOOLE_1:1,28;
  for r st r<x0 ex g st r<g & g<x0 & g in dom f by A2,A3,A5,Th3,XBOOLE_1:1;
  hence thesis by A1,A2,A4,A6,A7,Th34;
end;

theorem
  f1 is_right_divergent_to+infty_in x0 & (ex r st 0<r & ].x0,x0+r.[ c=
  dom f /\ dom f1 & for g st g in ].x0,x0+r.[ holds f1.g<= f.g) implies f
  is_right_divergent_to+infty_in x0
proof
  assume
A1: f1 is_right_divergent_to+infty_in x0;
  given r such that
A2: 0<r and
A3: ].x0,x0+r.[c=dom f/\dom f1 and
A4: for g st g in ].x0,x0+r.[ holds f1.g<=f.g;
A5: dom f/\dom f1 c=dom f by XBOOLE_1:17;
  then
A6: ].x0,x0+r.[=dom f/\].x0,x0+r.[ by A3,XBOOLE_1:1,28;
  dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
  then
A7: ].x0,x0+r.[=dom f1/\].x0,x0+r.[ by A3,XBOOLE_1:1,28;
  for r st x0<r ex g st g<r & x0<g & g in dom f by A2,A3,A5,Th4,XBOOLE_1:1;
  hence thesis by A1,A2,A4,A6,A7,Th35;
end;

theorem
  f1 is_right_divergent_to-infty_in x0 & (ex r st 0<r & ].x0,x0+r.[ c=
  dom f /\ dom f1 & for g st g in ].x0,x0+r.[ holds f.g<= f1.g) implies f
  is_right_divergent_to-infty_in x0
proof
  assume
A1: f1 is_right_divergent_to-infty_in x0;
  given r such that
A2: 0<r and
A3: ].x0,x0+r.[c=dom f/\dom f1 and
A4: for g st g in ].x0,x0+r.[ holds f.g<=f1.g;
A5: dom f/\dom f1 c=dom f by XBOOLE_1:17;
  then
A6: ].x0,x0+r.[=dom f/\].x0,x0+r.[ by A3,XBOOLE_1:1,28;
  dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
  then
A7: ].x0,x0+r.[=dom f1/\].x0,x0+r.[ by A3,XBOOLE_1:1,28;
  for r st x0<r ex g st g<r & x0<g & g in dom f by A2,A3,A5,Th4,XBOOLE_1:1;
  hence thesis by A1,A2,A4,A6,A7,Th36;
end;

definition
  let f,x0;
  assume
A1: f is_left_convergent_in x0;
  func lim_left(f,x0)-> Real means
  :Def7:
  for seq st seq is convergent & lim seq=x0 &
    rng seq c= dom f /\ left_open_halfline(x0)
   holds f/*seq is convergent & lim(f/*seq)=it;
  existence
   by A1;
  uniqueness
  proof
    defpred X[Nat,Real] means x0-1/($1+1)<$2 & $2<x0 & $2 in
    dom f;
    let g1,g2 be Real such that
A2: for seq st seq is convergent & lim seq=x0 & rng seq c=dom f/\
    left_open_halfline(x0) holds f/*seq is convergent & lim(f/*seq)=g1 and
A3: for seq st seq is convergent & lim seq=x0 & rng seq c=dom f/\
    left_open_halfline(x0) holds f/*seq is convergent & lim(f/*seq)=g2;
A4: now
      let n be Element of NAT;
      x0-1/(n+1)<x0 by Lm3;
      then consider g such that
A5:   x0-1/(n+1)<g and
A6:   g<x0 and
A7:   g in dom f by A1;
       reconsider g as Element of REAL by XREAL_0:def 1;
      take g;
      thus X[n,g] by A5,A6,A7;
    end;
    consider s be Real_Sequence such that
A8: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A4);
A9: for n being Nat holds X[n,s.n]
     proof let n;
      n in NAT by ORDINAL1:def 12;
      hence thesis by A8;
     end;
A10: rng s c=dom f/\left_open_halfline(x0) by A9,Th5;
A11: lim s=x0 by A9,Th5;
A12: s is convergent by A9,Th5;
    then lim(f/*s)=g1 by A11,A10,A2;
    hence thesis by A12,A11,A10,A3;
  end;
end;

definition
  let f,x0;
  assume
A1: f is_right_convergent_in x0;
  func lim_right(f,x0)-> Real means
  :Def8:
  for seq st seq is convergent & lim
seq=x0 & rng seq c= dom f /\ right_open_halfline(x0) holds f/*seq is convergent
  & lim(f/*seq)=it;
  existence
   by A1;
  uniqueness
  proof
    defpred X[Nat,Real] means x0<$2 & $2<x0+1/($1+1) & $2 in
    dom f;
    let g1,g2 be Real such that
A2: for seq st seq is convergent & lim seq=x0 & rng seq c=dom f/\
    right_open_halfline(x0) holds f/*seq is convergent & lim(f/*seq)=g1 and
A3: for seq st seq is convergent & lim seq=x0 & rng seq c=dom f/\
    right_open_halfline(x0) holds f/*seq is convergent & lim(f/*seq)=g2;
A4: now
      let n be Element of NAT;
      x0<x0+1/(n+1) by Lm3;
      then consider g such that
A5:   g<x0+(1/(n+1)) and
A6:   x0<g and
A7:   g in dom f by A1;
       reconsider g as Element of REAL by XREAL_0:def 1;
      take g;
      thus X[n,g] by A5,A6,A7;
    end;
    consider s be Real_Sequence such that
A8: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A4);
A9: for n being Nat holds X[n,s.n]
     proof let n;
      n in NAT by ORDINAL1:def 12;
      hence thesis by A8;
     end;
A10: rng s c=dom f/\right_open_halfline(x0) by A9,Th6;
A11: lim s=x0 by A9,Th6;
A12: s is convergent by A9,Th6;
    then lim(f/*s)=g1 by A11,A10,A2;
    hence thesis by A12,A11,A10,A3;
  end;
end;

theorem
  f is_left_convergent_in x0 implies (lim_left(f,x0)=g iff for g1 st 0<
  g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds |.f.r1-g.|<g1)
proof
  assume
A1: f is_left_convergent_in x0;
  thus lim_left(f,x0)=g implies for g1 st 0<g1 ex r st r<x0 & for r1 st r<r1 &
  r1<x0 & r1 in dom f holds |.f.r1-g.|<g1
  proof
    assume that
A2: lim_left(f,x0)=g and
A3: ex g1 st 0<g1 & for r st r<x0 ex r1 st r<r1 & r1<x0 & r1 in dom f
    & |.f.r1-g.|>=g1;
    consider g1 such that
A4: 0<g1 and
A5: for r st r<x0 ex r1 st r<r1 & r1<x0 & r1 in dom f & |.f.r1-g.|>= g1 by A3;
    defpred X[Nat,Real] means x0-1/($1+1)<$2 & $2<x0 & $2 in
    dom f & |.f.($2)-g.|>=g1;
A6: now
      let n be Element of NAT;
      x0-1/(n+1)<x0 by Lm3;
      then consider g2 such that
A7:   x0-1/(n+1)<g2 and
A8:   g2<x0 and
A9:   g2 in dom f and
A10:  |.f.g2-g.|>=g1 by A5;
       reconsider g2 as Element of REAL by XREAL_0:def 1;
      take g2;
      thus X[n,g2] by A7,A8,A9,A10;
    end;
    consider s be Real_Sequence such that
A11: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A6);
A12: for n being Nat holds X[n,s.n]
     proof let n;
      n in NAT by ORDINAL1:def 12;
      hence thesis by A11;
     end;
A13: rng s c=dom f/\left_open_halfline(x0) by A12,Th5;
A14: lim s=x0 by A12,Th5;
A15: s is convergent by A12,Th5;
    then
A16: lim(f/*s)=g by A1,A2,A14,A13,Def7;
    f/*s is convergent by A1,A15,A14,A13;
    then consider n such that
A17: for k st n<=k holds |.(f/*s).k-g.|<g1 by A4,A16,SEQ_2:def 7;
A18: |.(f/*s).n-g.|<g1 by A17;
A19: n in NAT by ORDINAL1:def 12;
    rng s c=dom f by A12,Th5;
    then |.f.(s.n)-g.|<g1 by A18,FUNCT_2:108,A19;
    hence contradiction by A12;
  end;
  assume
A20: for g1 st 0<g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f
  holds |.f.r1-g.|<g1;
  reconsider g as Real;
  now
    let s be Real_Sequence such that
A21: s is convergent and
A22: lim s=x0 and
A23: rng s c=dom f/\left_open_halfline(x0);
A24: dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
A25: now
      let g1 be Real;
      assume
A26:  0<g1;
      consider r such that
A27:  r<x0 and
A28:  for r1 st r<r1 & r1<x0 & r1 in dom f holds |.f.r1-g.|<g1 by A20,A26;
      consider n such that
A29:  for k st n<=k holds r<s.k by A21,A22,A27,Th1;
      take n;
      let k;
      assume
A30:  n<=k;
A31:  s.k in rng s by VALUED_0:28;
      then s.k in left_open_halfline(x0) by A23,XBOOLE_0:def 4;
      then s.k in {g2: g2<x0} by XXREAL_1:229;
      then
A32:  ex g2 st g2=s.k & g2<x0;
A33: k in NAT by ORDINAL1:def 12;
      s.k in dom f by A23,A31,XBOOLE_0:def 4;
      then |.f.(s.k)-g.|<g1 by A28,A29,A30,A32;
      hence |.(f/*s).k-g.|<g1 by A23,A24,FUNCT_2:108,XBOOLE_1:1,A33;
    end;
    hence f/*s is convergent by SEQ_2:def 6;
    hence lim(f/*s)=g by A25,SEQ_2:def 7;
  end;
  hence thesis by A1,Def7;
end;

theorem
  f is_right_convergent_in x0 implies (lim_right(f,x0)=g iff for g1 st 0
  <g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds |.f.r1-g.|<g1)
proof
  assume
A1: f is_right_convergent_in x0;
  thus lim_right(f,x0)=g implies for g1 st 0<g1 ex r st x0<r & for r1 st r1<r
  & x0<r1 & r1 in dom f holds |.f.r1-g.|<g1
  proof
    assume that
A2: lim_right(f,x0)=g and
A3: ex g1 st 0<g1 & for r st x0<r ex r1 st r1<r & x0<r1 & r1 in dom f
    & |.f.r1-g.|>=g1;
    consider g1 such that
A4: 0<g1 and
A5: for r st x0<r ex r1 st r1<r & x0<r1 & r1 in dom f & |.f.r1-g.|>= g1 by A3;
    defpred X[Nat,Real] means x0<$2 & $2<x0+1/($1+1) & $2 in
    dom f & g1<=|.f.($2)-g.|;
A6: now
      let n be Element of NAT;
      x0<x0+1/(n+1) by Lm3;
      then consider r1 such that
A7:   r1<x0+(1/(n+1)) and
A8:   x0<r1 and
A9:   r1 in dom f and
A10:  g1<=|.f.r1-g.| by A5;
       reconsider r1 as Element of REAL by XREAL_0:def 1;
      take r1;
      thus X[n,r1] by A7,A8,A9,A10;
    end;
    consider s be Real_Sequence such that
A11: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A6);
A12: for n being Nat holds X[n,s.n]
     proof let n;
      n in NAT by ORDINAL1:def 12;
      hence thesis by A11;
     end;
A13: rng s c=dom f/\right_open_halfline(x0) by A12,Th6;
A14: lim s=x0 by A12,Th6;
A15: s is convergent by A12,Th6;
    then
A16: lim(f/*s)=g by A1,A2,A14,A13,Def8;
    f/*s is convergent by A1,A15,A14,A13;
    then consider n such that
A17: for k st n<=k holds |.(f/*s).k-g.|<g1 by A4,A16,SEQ_2:def 7;
A18: |.(f/*s).n-g.|<g1 by A17;
A19: n in NAT by ORDINAL1:def 12;
    rng s c=dom f by A12,Th6;
    then |.f.(s.n)-g.|<g1 by A18,FUNCT_2:108,A19;
    hence contradiction by A12;
  end;
  assume
A20: for g1 st 0<g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f
  holds |.f.r1-g.|<g1;
  reconsider g as Real;
  now
    let s be Real_Sequence such that
A21: s is convergent and
A22: lim s=x0 and
A23: rng s c=dom f/\right_open_halfline(x0);
A24: dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
A25: now
      let g1 be Real;
      assume
A26:  0<g1;
      consider r such that
A27:  x0<r and
A28:  for r1 st r1<r & x0<r1 & r1 in dom f holds |.f.r1-g.|<g1 by A20,A26;
      consider n such that
A29:  for k st n<=k holds s.k<r by A21,A22,A27,Th2;
      take n;
      let k;
      assume
A30:  n<=k;
A31:  s.k in rng s by VALUED_0:28;
      then s.k in right_open_halfline(x0) by A23,XBOOLE_0:def 4;
      then s.k in {g2: x0<g2} by XXREAL_1:230;
      then
A32:  ex g2 st g2=s.k & x0<g2;
A33: k in NAT by ORDINAL1:def 12;
      s.k in dom f by A23,A31,XBOOLE_0:def 4;
      then |.f.(s.k)-g.|<g1 by A28,A29,A30,A32;
      hence |.(f/*s).k-g.|<g1 by A23,A24,FUNCT_2:108,XBOOLE_1:1,A33;
    end;
    hence f/*s is convergent by SEQ_2:def 6;
    hence lim(f/*s)=g by A25,SEQ_2:def 7;
  end;
  hence thesis by A1,Def8;
end;

theorem Th43:
  f is_left_convergent_in x0 implies r(#)f is_left_convergent_in
  x0 & lim_left(r(#)f,x0)=r*(lim_left(f,x0))
proof
  assume
A1: f is_left_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)/\left_open_halfline(x0);
A6: rng seq c=dom f/\left_open_halfline(x0) by A5,VALUED_1:def 5;
A7: dom f/\left_open_halfline(x0) c=dom f by XBOOLE_1:17;
    then
A8: r(#) (f/*seq)=(r(#)f)/*seq by A6,RFUNCT_2:9,XBOOLE_1:1;
A9: f/*seq is convergent by A1,A3,A4,A6;
    then r(#)(f/*seq) is convergent;
    hence (r(#)f)/*seq is convergent by A6,A7,RFUNCT_2:9,XBOOLE_1:1;
    lim(f/*seq)=lim_left(f,x0) by A1,A3,A4,A6,Def7;
    hence lim((r(#)f)/*seq)=r*(lim_left(f,x0)) by A9,A8,SEQ_2:8;
  end;
  now
    let r1;
    assume r1<x0;
    then consider g such that
A10: r1<g and
A11: g<x0 and
A12: g in dom f by A1;
    take g;
    thus r1<g & g<x0 & g in dom(r(#)f) by A10,A11,A12,VALUED_1:def 5;
  end;
  hence r(#)f is_left_convergent_in x0 by A2;
  hence thesis by A2,Def7;
end;

theorem Th44:
  f is_left_convergent_in x0 implies -f is_left_convergent_in x0 &
  lim_left(-f,x0)=-(lim_left(f,x0))
proof
  assume
A1: f is_left_convergent_in x0;
  thus -f is_left_convergent_in x0 by A1,Th43;
  thus lim_left(-f,x0)=(-1)*(lim_left(f,x0)) by A1,Th43
    .=-(lim_left(f,x0));
end;

theorem Th45:
  f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & (for
  r st r<x0 ex g st r<g & g<x0 & g in dom(f1+f2)) implies f1+f2
  is_left_convergent_in x0 & lim_left(f1+f2,x0)=lim_left(f1,x0)+lim_left(f2,x0)
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_left_convergent_in x0 and
A3: for r st r<x0 ex g st r<g & g<x0 & g 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)/\left_open_halfline(x0);
A8: dom(f1+f2)=dom f1/\dom f2 by A7,Lm4;
A9: rng seq c=dom f1/\left_open_halfline(x0) by A7,Lm4;
A10: rng seq c=dom f2/\left_open_halfline(x0) by A7,Lm4;
    then
A11: lim(f2/*seq)=lim_left(f2,x0) by A2,A5,A6,Def7;
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;
    lim(f1/*seq)=lim_left(f1,x0) by A1,A5,A6,A9,Def7;
    hence lim((f1+f2)/*seq)=lim_left(f1,x0)+lim_left(f2,x0) by A14,A12,A11,A13,
SEQ_2:6;
  end;
  hence f1+f2 is_left_convergent_in x0 by A3;
  hence thesis by A4,Def7;
end;

theorem
  f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & (for r st
r<x0 ex g st r<g & g<x0 & g in dom(f1-f2)) implies f1-f2 is_left_convergent_in
  x0 & lim_left(f1-f2,x0)=(lim_left(f1,x0))-(lim_left(f2,x0))
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_left_convergent_in x0 and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f1-f2);
A4: -f2 is_left_convergent_in x0 by A2,Th44;
  hence f1-f2 is_left_convergent_in x0 by A1,A3,Th45;
  thus lim_left(f1-f2,x0)=lim_left(f1,x0)+lim_left(-f2,x0) by A1,A3,A4,Th45
    .=(lim_left(f1,x0))+-lim_left(f2,x0) by A2,Th44
    .=(lim_left(f1,x0))-lim_left(f2,x0);
end;

theorem
  f is_left_convergent_in x0 & f"{0}={} & lim_left(f,x0)<>0 implies f^
  is_left_convergent_in x0 & lim_left(f^,x0)=(lim_left(f,x0))"
proof
  assume that
A1: f is_left_convergent_in x0 and
A2: f"{0}={} and
A3: lim_left(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^)/\left_open_halfline(x0);
A9: lim(f/*seq)=lim_left(f,x0) by A1,A4,A6,A7,A8,Def7;
A10: dom f/\left_open_halfline(x0) c=dom f by XBOOLE_1:17;
    then
A11: rng seq c=dom f by A4,A8,XBOOLE_1:1;
A12: f/*seq is convergent by A1,A4,A6,A7,A8;
A13: (f/*seq)"=(f^)/*seq by A4,A8,A10,RFUNCT_2:12,XBOOLE_1:1;
    hence (f^)/*seq is convergent by A3,A4,A12,A9,A11,RFUNCT_2:11,SEQ_2:21;
    thus lim((f^)/*seq)=(lim_left(f,x0))" by A3,A4,A12,A9,A11,A13,RFUNCT_2:11
,SEQ_2:22;
  end;
  for r st r<x0 ex g st r<g & g<x0 & g in dom(f^) by A1,A4;
  hence f^ is_left_convergent_in x0 by A5;
  hence thesis by A5,Def7;
end;

theorem
  f is_left_convergent_in x0 implies abs(f) is_left_convergent_in x0 &
  lim_left(abs(f),x0)=|.lim_left(f,x0).|
proof
  assume
A1: f is_left_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))/\left_open_halfline(x0);
A6: rng seq c=dom f/\left_open_halfline(x0) by A5,VALUED_1:def 11;
    dom f/\left_open_halfline(x0) c=dom f by XBOOLE_1:17;
    then rng seq c=dom f by A6,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_left(f,x0) by A1,A3,A4,A6,Def7;
    hence lim((abs f)/*seq)=|.lim_left(f,x0).| by A8,A7,SEQ_4:14;
  end;
  now
    let r;
    assume r<x0;
    then consider g such that
A9: r<g and
A10: g<x0 and
A11: g in dom f by A1;
    take g;
    thus r<g & g<x0 & g in dom abs(f) by A9,A10,A11,VALUED_1:def 11;
  end;
  hence abs(f) is_left_convergent_in x0 by A2;
  hence thesis by A2,Def7;
end;

theorem Th49:
  f is_left_convergent_in x0 & lim_left(f,x0)<>0 & (for r st r<x0
ex g st r<g & g<x0 & g in dom f & f.g<>0) implies f^ is_left_convergent_in x0 &
  lim_left(f^,x0)=(lim_left(f,x0))"
proof
  assume that
A1: f is_left_convergent_in x0 and
A2: lim_left(f,x0)<>0 and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0;
A4: dom f\f"{0}=dom(f^) by RFUNCT_1:def 2;
A5: now
A6: dom(f^)c=dom f by A4,XBOOLE_1:36;
    let seq such that
A7: seq is convergent and
A8: lim seq=x0 and
A9: rng seq c=dom(f^)/\left_open_halfline(x0);
A10: dom(f^)/\left_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
    then
A11: f/*seq is non-zero by A9,RFUNCT_2:11,XBOOLE_1:1;
    rng seq c=dom(f^) by A9,A10,XBOOLE_1:1;
    then
A12: rng seq c=dom f by A6,XBOOLE_1:1;
    dom(f^)/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
    then rng seq c=left_open_halfline(x0) by A9,XBOOLE_1:1;
    then
A13: rng seq c=dom f/\left_open_halfline(x0) by A12,XBOOLE_1:19;
    then
A14: lim(f/*seq)=lim_left(f,x0) by A1,A7,A8,Def7;
A15: (f/*seq)"=(f^)/*seq by A9,A10,RFUNCT_2:12,XBOOLE_1:1;
A16: f/*seq is convergent by A1,A7,A8,A13;
    hence (f^)/*seq is convergent by A2,A14,A11,A15,SEQ_2:21;
    thus lim((f^)/*seq)=(lim_left(f,x0))" by A2,A16,A14,A11,A15,SEQ_2:22;
  end;
  now
    let r;
    assume r<x0;
    then consider g such that
A17: r<g and
A18: g<x0 and
A19: g in dom f and
A20: f.g<>0 by A3;
    take g;
    not f.g in {0} by A20,TARSKI:def 1;
    then not g in f"{0} by FUNCT_1:def 7;
    hence r<g & g<x0 & g in dom(f^) by A4,A17,A18,A19,XBOOLE_0:def 5;
  end;
  hence f^ is_left_convergent_in x0 by A5;
  hence thesis by A5,Def7;
end;

theorem Th50:
  f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & (for
  r st r<x0 ex g st r<g & g<x0 & g in dom(f1(#)f2)) implies f1(#)f2
is_left_convergent_in x0 & lim_left(f1(#)f2,x0)=(lim_left(f1,x0))*(lim_left(f2,
  x0))
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_left_convergent_in x0 and
A3: for r st r<x0 ex g st r<g & g<x0 & g 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)/\left_open_halfline(x0);
A8: dom(f1(#)f2)=dom f1/\dom f2 by A7,Lm2;
A9: rng seq c=dom f1/\left_open_halfline(x0) by A7,Lm2;
A10: rng seq c=dom f2/\left_open_halfline(x0) by A7,Lm2;
    then
A11: lim(f2/*seq)=lim_left(f2,x0) by A2,A5,A6,Def7;
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;
    lim(f1/*seq)=lim_left(f1,x0) by A1,A5,A6,A9,Def7;
    hence lim((f1(#)f2)/*seq)=lim_left(f1,x0)*lim_left(f2,x0) by A14,A12,A11
,A13,SEQ_2:15;
  end;
  hence f1(#) f2 is_left_convergent_in x0 by A3;
  hence thesis by A4,Def7;
end;

theorem
  f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left(
f2,x0 ) <> 0 & (for r st r<x0 ex g st r<g & g<x0 & g in dom(f1/f2)) implies f1/
f2 is_left_convergent_in x0 & lim_left(f1/f2,x0)=(lim_left(f1,x0))/(lim_left(f2
  ,x0))
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_left_convergent_in x0 and
A3: lim_left(f2,x0)<>0 and
A4: for r st r<x0 ex g st r<g & g<x0 & g in dom(f1/f2);
A5: now
    let r;
    assume r<x0;
    then consider g such that
A6: r<g and
A7: g<x0 and
A8: g in dom(f1/f2) by A4;
    take g;
    thus r<g & g<x0 by A6,A7;
    dom(f1/f2)=dom f1/\(dom f2\f2"{0}) by RFUNCT_1:def 1;
    then
A9: g in dom f2\f2"{0} by A8,XBOOLE_0:def 4;
    then
A10: not g in f2"{0} by XBOOLE_0:def 5;
    g in dom f2 by A9,XBOOLE_0:def 5;
    then not f2.g in {0} by A10,FUNCT_1:def 7;
    hence g in dom f2 & f2.g<>0 by A9,TARSKI:def 1,XBOOLE_0:def 5;
  end;
  then
A11: f2^ is_left_convergent_in x0 by A2,A3,Th49;
A12: f1/f2=f1(#)(f2^) by RFUNCT_1:31;
  hence f1/f2 is_left_convergent_in x0 by A1,A4,A11,Th50;
  lim_left(f2^,x0)=(lim_left(f2,x0))" by A2,A3,A5,Th49;
  hence
  lim_left(f1/f2,x0)=lim_left(f1,x0)*((lim_left(f2,x0))") by A1,A4,A12,A11,Th50
    .=lim_left(f1,x0)/(lim_left(f2,x0)) by XCMPLX_0:def 9;
end;

theorem Th52:
  f is_right_convergent_in x0 implies r(#)f is_right_convergent_in
  x0 & lim_right(r(#)f,x0)=r*(lim_right(f,x0))
proof
  assume
A1: f is_right_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)/\right_open_halfline(x0);
A6: rng seq c=dom f/\right_open_halfline(x0) by A5,VALUED_1:def 5;
A7: dom f/\right_open_halfline(x0) c=dom f by XBOOLE_1:17;
    then
A8: r (#)(f/*seq)=(r(#)f)/*seq by A6,RFUNCT_2:9,XBOOLE_1:1;
A9: f/*seq is convergent by A1,A3,A4,A6;
    then r(#)(f/*seq) is convergent;
    hence (r(#)f)/*seq is convergent by A6,A7,RFUNCT_2:9,XBOOLE_1:1;
    lim(f/*seq)=lim_right(f,x0) by A1,A3,A4,A6,Def8;
    hence lim((r(#)f)/*seq)=r*(lim_right(f,x0)) by A9,A8,SEQ_2:8;
  end;
  now
    let r1;
    assume x0<r1;
    then consider g such that
A10: g<r1 and
A11: x0<g and
A12: g in dom f by A1;
    take g;
    thus g<r1 & x0<g & g in dom(r(#)f) by A10,A11,A12,VALUED_1:def 5;
  end;
  hence r(#) f is_right_convergent_in x0 by A2;
  hence thesis by A2,Def8;
end;

theorem Th53:
  f is_right_convergent_in x0 implies -f is_right_convergent_in x0
  & lim_right(-f,x0)=-(lim_right(f,x0))
proof
  assume
A1: f is_right_convergent_in x0;
  thus -f is_right_convergent_in x0 by A1,Th52;
  thus lim_right(-f,x0)=(-1)*(lim_right(f,x0)) by A1,Th52
    .=-(lim_right(f,x0));
end;

theorem Th54:
  f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & (
  for r st x0<r ex g st g<r & x0<g & g in dom(f1+f2)) implies f1+f2
is_right_convergent_in x0 & lim_right(f1+f2,x0)=(lim_right(f1,x0))+(lim_right(
  f2,x0))
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_right_convergent_in x0 and
A3: for r st x0<r ex g st g<r & x0<g & g 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)/\right_open_halfline(x0);
A8: dom(f1+f2)=dom f1/\dom f2 by A7,Lm4;
A9: rng seq c=dom f1/\right_open_halfline(x0) by A7,Lm4;
A10: rng seq c=dom f2/\right_open_halfline(x0) by A7,Lm4;
    then
A11: lim(f2/*seq)=lim_right(f2,x0) by A2,A5,A6,Def8;
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;
    lim(f1/*seq)=lim_right(f1,x0) by A1,A5,A6,A9,Def8;
    hence lim((f1+f2)/*seq)=lim_right(f1,x0)+lim_right(f2,x0) by A14,A12,A11
,A13,SEQ_2:6;
  end;
  hence f1+f2 is_right_convergent_in x0 by A3;
  hence thesis by A4,Def8;
end;

theorem
  f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & (for r
  st x0<r ex g st g<r & x0<g & g in dom(f1-f2)) implies f1-f2
is_right_convergent_in x0 & lim_right(f1-f2,x0)=(lim_right(f1,x0))-(lim_right(
  f2,x0))
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_right_convergent_in x0 and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f1-f2);
A4: -f2 is_right_convergent_in x0 by A2,Th53;
  hence f1-f2 is_right_convergent_in x0 by A1,A3,Th54;
  thus lim_right(f1-f2,x0)=lim_right(f1,x0)+lim_right(-f2,x0) by A1,A3,A4,Th54
    .=(lim_right(f1,x0))+-lim_right(f2,x0) by A2,Th53
    .=(lim_right(f1,x0))-lim_right(f2,x0);
end;

theorem
  f is_right_convergent_in x0 & f"{0}={} & lim_right(f,x0)<>0 implies f^
  is_right_convergent_in x0 & lim_right(f^,x0)=(lim_right(f,x0))"
proof
  assume that
A1: f is_right_convergent_in x0 and
A2: f"{0}={} and
A3: lim_right(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^)/\right_open_halfline(x0);
A9: lim(f/*seq)=lim_right(f,x0) by A1,A4,A6,A7,A8,Def8;
A10: dom f/\right_open_halfline(x0) c=dom f by XBOOLE_1:17;
    then
A11: rng seq c=dom f by A4,A8,XBOOLE_1:1;
A12: f/*seq is convergent by A1,A4,A6,A7,A8;
A13: (f/*seq)"=(f^)/*seq by A4,A8,A10,RFUNCT_2:12,XBOOLE_1:1;
    hence (f^)/*seq is convergent by A3,A4,A12,A9,A11,RFUNCT_2:11,SEQ_2:21;
    thus lim((f^)/*seq)=(lim_right(f,x0))" by A3,A4,A12,A9,A11,A13,RFUNCT_2:11
,SEQ_2:22;
  end;
  for r st x0<r ex g st g<r & x0<g & g in dom(f^) by A1,A4;
  hence f^ is_right_convergent_in x0 by A5;
  hence thesis by A5,Def8;
end;

theorem
  f is_right_convergent_in x0 implies abs(f) is_right_convergent_in x0 &
  lim_right(abs(f),x0)=|.lim_right(f,x0).|
proof
  assume
A1: f is_right_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))/\right_open_halfline(x0);
A6: rng seq c=dom f/\right_open_halfline(x0) by A5,VALUED_1:def 11;
    dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
    then rng seq c=dom f by A6,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_right(f,x0) by A1,A3,A4,A6,Def8;
    hence lim((abs f)/*seq)=|.lim_right(f,x0).| by A8,A7,SEQ_4:14;
  end;
  now
    let r;
    assume x0<r;
    then consider g such that
A9: g<r and
A10: x0<g and
A11: g in dom f by A1;
    take g;
    thus g<r & x0<g & g in dom abs(f) by A9,A10,A11,VALUED_1:def 11;
  end;
  hence abs(f) is_right_convergent_in x0 by A2;
  hence thesis by A2,Def8;
end;

theorem Th58:
  f is_right_convergent_in x0 & lim_right(f,x0)<>0 & (for r st x0<
  r ex g st g<r & x0<g & g in dom f & f.g<>0) implies f^ is_right_convergent_in
  x0 & lim_right(f^,x0)=(lim_right(f,x0))"
proof
  assume that
A1: f is_right_convergent_in x0 and
A2: lim_right(f,x0)<>0 and
A3: for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0;
A4: dom f\f"{0}=dom(f^) by RFUNCT_1:def 2;
A5: now
A6: dom(f^) c=dom f by A4,XBOOLE_1:36;
    let seq such that
A7: seq is convergent and
A8: lim seq=x0 and
A9: rng seq c=dom(f^)/\right_open_halfline(x0);
A10: dom(f^)/\right_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
    then
A11: f/*seq is non-zero by A9,RFUNCT_2:11,XBOOLE_1:1;
    rng seq c=dom(f^) by A9,A10,XBOOLE_1:1;
    then
A12: rng seq c=dom f by A6,XBOOLE_1:1;
    dom(f^)/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
    then rng seq c=right_open_halfline(x0) by A9,XBOOLE_1:1;
    then
A13: rng seq c=dom f/\right_open_halfline(x0) by A12,XBOOLE_1:19;
    then
A14: lim(f/*seq)=lim_right(f,x0) by A1,A7,A8,Def8;
A15: (f/*seq)"=(f^)/*seq by A9,A10,RFUNCT_2:12,XBOOLE_1:1;
A16: f/*seq is convergent by A1,A7,A8,A13;
    hence (f^)/*seq is convergent by A2,A14,A11,A15,SEQ_2:21;
    thus lim((f^)/*seq)=(lim_right(f,x0))" by A2,A16,A14,A11,A15,SEQ_2:22;
  end;
  now
    let r;
    assume x0<r;
    then consider g such that
A17: g<r and
A18: x0<g and
A19: g in dom f and
A20: f.g<>0 by A3;
    take g;
    not f.g in {0} by A20,TARSKI:def 1;
    then not g in f"{0} by FUNCT_1:def 7;
    hence g<r & x0<g & g in dom(f^) by A4,A17,A18,A19,XBOOLE_0:def 5;
  end;
  hence f^ is_right_convergent_in x0 by A5;
  hence thesis by A5,Def8;
end;

theorem Th59:
  f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & (
  for r st x0<r ex g st g<r & x0<g & g in dom(f1(#)f2)) implies f1(#)f2
is_right_convergent_in x0 & lim_right(f1(#)f2,x0)=(lim_right(f1,x0))*(lim_right
  (f2,x0))
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_right_convergent_in x0 and
A3: for r st x0<r ex g st g<r & x0<g & g 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)/\right_open_halfline(x0);
A8: dom(f1(#)f2)=dom f1/\dom f2 by A7,Lm2;
A9: rng seq c=dom f1/\right_open_halfline(x0) by A7,Lm2;
A10: rng seq c=dom f2/\right_open_halfline(x0) by A7,Lm2;
    then
A11: lim(f2/*seq)=lim_right(f2,x0) by A2,A5,A6,Def8;
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;
    lim(f1/*seq)=lim_right(f1,x0) by A1,A5,A6,A9,Def8;
    hence lim((f1(#) f2)/*seq)=lim_right(f1,x0)*lim_right(f2,x0) by A14,A12,A11
,A13,SEQ_2:15;
  end;
  hence f1(#) f2 is_right_convergent_in x0 by A3;
  hence thesis by A4,Def8;
end;

theorem
  f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
  lim_right(f2,x0)<>0 & (for r st x0<r ex g st g<r & x0<g & g in dom(f1/f2))
implies f1/f2 is_right_convergent_in x0 & lim_right(f1/f2,x0)=(lim_right(f1,x0)
  )/(lim_right(f2,x0))
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_right_convergent_in x0 and
A3: lim_right(f2,x0)<>0 and
A4: for r st x0<r ex g st g<r & x0<g & g in dom(f1/f2);
A5: now
    let r;
    assume x0<r;
    then consider g such that
A6: g<r and
A7: x0<g and
A8: g in dom(f1/f2) by A4;
    take g;
    thus g<r & x0<g by A6,A7;
    dom(f1/f2)=dom f1/\(dom f2\f2"{0}) by RFUNCT_1:def 1;
    then
A9: g in dom f2\f2"{0} by A8,XBOOLE_0:def 4;
    then
A10: not g in f2"{0} by XBOOLE_0:def 5;
    g in dom f2 by A9,XBOOLE_0:def 5;
    then not f2.g in {0} by A10,FUNCT_1:def 7;
    hence g in dom f2 & f2.g<>0 by A9,TARSKI:def 1,XBOOLE_0:def 5;
  end;
  then
A11: f2^ is_right_convergent_in x0 by A2,A3,Th58;
A12: f1/f2=f1(#)(f2^) by RFUNCT_1:31;
  hence f1/f2 is_right_convergent_in x0 by A1,A4,A11,Th59;
  lim_right(f2^,x0)=(lim_right(f2,x0)) " by A2,A3,A5,Th58;
  hence lim_right(f1/f2,x0)=lim_right(f1,x0)*((lim_right(f2,x0))") by A1,A4,A12
,A11,Th59
    .=lim_right(f1,x0)/(lim_right(f2,x0)) by XCMPLX_0:def 9;
end;

theorem
  f1 is_left_convergent_in x0 & lim_left(f1,x0)=0 & (for r st r<x0 ex g
st r<g & g<x0 & g in dom(f1(#)f2)) & (ex r st 0<r & f2|].x0-r,x0.[ is bounded)
  implies f1(#)f2 is_left_convergent_in x0 & lim_left(f1(#)f2,x0)=0
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: lim_left(f1,x0)=0 and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f1(#)f2);
  given r such that
A4: 0<r and
A5: f2|].x0-r,x0.[ is bounded;
  consider g be Real such that
A6: for r1 being object st r1 in ].x0-r,x0.[/\dom f2 holds |.f2.r1.|<=g by A5,
RFUNCT_1:73;
A7: now
    set L=left_open_halfline(x0);
    let s be Real_Sequence;
    assume that
A8: s is convergent and
A9: lim s=x0 and
A10: rng s c=dom(f1(#)f2)/\left_open_halfline(x0);
    x0-r<x0 by A4,Lm1;
    then consider k such that
A11: for n st k<=n holds x0-r<s.n by A8,A9,Th1;
A12: rng(s^\k)c=rng s by VALUED_0:21;
A13: 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 A13,A12,XBOOLE_1:1;
    then
A14: (f1/*(s^\k))(#)(f2/*(s^\k))=(f1(#)f2)/*(s^\k) by RFUNCT_2:8
      .=((f1(#)f2)/*s)^\k by A13,VALUED_0:27;
    rng s c=dom f1/\left_open_halfline(x0) by A10,Lm2;
    then
A15: rng(s^\k)c=dom f1/\L by A12,XBOOLE_1:1;
A16: lim(s^\k)=x0 by A8,A9,SEQ_4:20;
    then
A17: f1/*(s^\k) is convergent by A1,A8,A15;
    rng s c=left_open_halfline(x0) by A10,Lm2;
    then
A18: rng(s^\k)c=L by A12,XBOOLE_1:1;
A19: rng s c=dom f2 by A10,Lm2;
    then
A20: rng(s^\k)c=dom f2 by A12,XBOOLE_1:1;
    now
      set t=|.g.|+1;
      0<=|.g.| by COMPLEX1:46;
      hence 0<t;
      let n;
A21: n in NAT by ORDINAL1:def 12;
      x0-r<s.(n+k) by A11,NAT_1:12;
      then
A22:  x0-r<(s^\k).n by NAT_1:def 3;
A23:  (s^\k).n in rng(s^\k) by VALUED_0:28;
      then (s^\k).n in L by A18;
      then (s^\k).n in {g1: g1<x0} by XXREAL_1:229;
      then ex g1 st g1=(s^\k).n & g1<x0;
      then (s^\k).n in {g2: x0-r<g2 & g2<x0} by A22;
      then (s^\k).n in ].x0-r,x0.[ by RCOMP_1:def 2;
      then (s^\k).n in ].x0-r,x0.[/\dom f2 by A20,A23,XBOOLE_0:def 4;
      then |.f2.((s^\k).n).|<=g by A6;
      then
A24:  |.(f2/*(s^\k)).n.|<= g by A19,A12,FUNCT_2:108,XBOOLE_1:1,A21;
      g<=|.g.| by ABSVALUE:4;
      then g<t by Lm1;
      hence |.(f2/*(s^\k)).n.|<t by A24,XXREAL_0:2;
    end;
    then
A25: f2/*(s^\k) is bounded by SEQ_2:3;
A26: lim(f1/*(s^\k))=0 by A1,A2,A8,A16,A15,Def7;
    then
A27: (f1/*(s^\k))(#)(f2/*(s^\k)) is convergent by A17,A25,SEQ_2:25;
    hence (f1(#)f2)/*s is convergent by A14,SEQ_4:21;
    lim((f1/*(s^\k))(#)(f2/*(s^\k)))=0 by A17,A26,A25,SEQ_2:26;
    hence lim((f1(#)f2)/*s)=0 by A27,A14,SEQ_4:22;
  end;
  hence f1(#) f2 is_left_convergent_in x0 by A3;
  hence thesis by A7,Def7;
end;

theorem
  f1 is_right_convergent_in x0 & lim_right(f1,x0)=0 & (for r st x0<r ex
g st g<r & x0<g & g in dom(f1(#)f2)) & (ex r st 0<r & f2|].x0,x0+r.[ is bounded
  ) implies f1(#)f2 is_right_convergent_in x0 & lim_right(f1(#)f2,x0)=0
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: lim_right(f1,x0)=0 and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f1(#)f2);
  given r such that
A4: 0<r and
A5: f2|].x0,x0+r.[ is bounded;
  consider g be Real such that
A6: for r1 being object st r1 in ].x0,x0+r.[/\dom f2 holds |.f2.r1.|<=g by A5,
RFUNCT_1:73;
A7: now
    set L=right_open_halfline(x0);
    let s be Real_Sequence;
    assume that
A8: s is convergent and
A9: lim s=x0 and
A10: rng s c=dom(f1(#)f2)/\right_open_halfline(x0);
    x0<x0+r by A4,Lm1;
    then consider k such that
A11: for n st k<=n holds s.n<x0+r by A8,A9,Th2;
A12: rng(s^\k)c=rng s by VALUED_0:21;
A13: 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 A13,A12,XBOOLE_1:1;
    then
A14: (f1/*(s^\k))(#)(f2/*(s^\k))=(f1(#)f2)/*(s^\k) by RFUNCT_2:8
      .=((f1(#)f2)/*s)^\k by A13,VALUED_0:27;
    rng s c=dom f1/\right_open_halfline(x0) by A10,Lm2;
    then
A15: rng(s^\k)c=dom f1/\L by A12,XBOOLE_1:1;
A16: lim(s^\k)=x0 by A8,A9,SEQ_4:20;
    then
A17: f1/*(s^\k) is convergent by A1,A8,A15;
    rng s c=right_open_halfline(x0) by A10,Lm2;
    then
A18: rng(s^\k)c=L by A12,XBOOLE_1:1;
A19: rng s c=dom f2 by A10,Lm2;
    then
A20: rng(s^\k)c=dom f2 by A12,XBOOLE_1:1;
    now
      set t=|.g.|+1;
      0<=|.g.| by COMPLEX1:46;
      hence 0<t;
      let n;
A21: n in NAT by ORDINAL1:def 12;
      s.(n+k)<x0+r by A11,NAT_1:12;
      then
A22:  (s^\k).n<x0+r by NAT_1:def 3;
A23:  (s^\k).n in rng(s^\k) by VALUED_0:28;
      then (s^\k).n in L by A18;
      then (s^\k).n in {g1: x0<g1} by XXREAL_1:230;
      then ex g1 st g1=(s^\k).n & x0<g1;
      then (s^\k).n in {g2: x0<g2 & g2<x0+r} by A22;
      then (s^\k).n in ].x0,x0+r.[ by RCOMP_1:def 2;
      then (s^\k).n in ].x0,x0+r.[/\dom f2 by A20,A23,XBOOLE_0:def 4;
      then |.f2.((s^\k).n).|<=g by A6;
      then
A24:  |.(f2/*(s^\k)).n.|<= g by A19,A12,FUNCT_2:108,XBOOLE_1:1,A21;
      g<=|.g.| by ABSVALUE:4;
      then g<t by Lm1;
      hence |.(f2/*(s^\k)).n.|<t by A24,XXREAL_0:2;
    end;
    then
A25: f2/*(s^\k) is bounded by SEQ_2:3;
A26: lim(f1/*(s^\k))=0 by A1,A2,A8,A16,A15,Def8;
    then
A27: (f1/*(s^\k))(#)(f2/*(s^\k)) is convergent by A17,A25,SEQ_2:25;
    hence (f1(#)f2)/*s is convergent by A14,SEQ_4:21;
    lim((f1/*(s^\k))(#)(f2/*(s^\k)))=0 by A17,A26,A25,SEQ_2:26;
    hence lim((f1(#)f2)/*s)=0 by A27,A14,SEQ_4:22;
  end;
  hence f1(#) f2 is_right_convergent_in x0 by A3;
  hence thesis by A7,Def8;
end;

theorem Th63:
  f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
lim_left(f1,x0)=lim_left(f2,x0) & (for r st r<x0 ex g st r<g & g<x0 & g in dom
f) & (ex r st 0<r & (for g st g in dom f /\ ].x0-r,x0.[ holds f1.g<=f.g & f.g<=
f2.g) & ((dom f1 /\ ].x0-r,x0.[ c= dom f2 /\ ].x0-r,x0.[ & dom f /\ ].x0-r,x0.[
c= dom f1 /\ ].x0-r,x0.[) or (dom f2 /\ ].x0-r,x0.[ c= dom f1 /\ ].x0-r,x0.[ &
  dom f /\ ].x0-r,x0.[ c= dom f2 /\ ].x0-r,x0.[))) implies f
  is_left_convergent_in x0 & lim_left(f,x0)=lim_left(f1,x0)
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_left_convergent_in x0 and
A3: lim_left(f1,x0)=lim_left(f2,x0) and
A4: for r st r<x0 ex g st r<g & g<x0 & g in dom f;
  given r1 such that
A5: 0<r1 and
A6: for g st g in dom f/\].x0-r1,x0.[ holds f1.g<=f.g & f.g<=f2.g and
A7: dom f1/\].x0-r1,x0.[c=dom f2/\].x0-r1,x0.[ & dom f/\].x0-r1,x0.[c=
dom f1/\].x0-r1,x0.[ or dom f2/\].x0-r1,x0.[c=dom f1/\].x0-r1,x0.[ & dom f/\].
  x0-r1,x0.[c=dom f2/\].x0-r1,x0.[;
  now
    per cases by A7;
    suppose
A8:   dom f1/\].x0-r1,x0.[c=dom f2/\].x0-r1,x0.[ & dom f/\].x0-r1,x0.[
      c=dom f1/\].x0-r1,x0.[;
A9:   now
        let seq;
        assume that
A10:    seq is convergent and
A11:    lim seq=x0 and
A12:    rng seq c=dom f/\left_open_halfline(x0);
        x0-r1<lim seq by A5,A11,Lm1;
        then consider k such that
A13:    for n st k<=n holds x0-r1<seq.n by A10,Th1;
A14:    rng(seq^\k)c=rng seq by VALUED_0:21;
        dom f/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
        then rng seq c=left_open_halfline(x0) by A12,XBOOLE_1:1;
        then
A15:    rng(seq^\k)c=left_open_halfline(x0) by A14,XBOOLE_1:1;
        now
          let x be object;
          assume
A16:      x in rng(seq^\k);
          then consider n being Element of NAT such that
A17:      x=(seq^\k).n by FUNCT_2:113;
          (seq^\k).n in left_open_halfline(x0) by A15,A16,A17;
          then (seq^\k).n in {g: g<x0} by XXREAL_1:229;
          then
A18:      ex g st g=(seq^\k).n & g<x0;
          x0-r1<seq.(n+k) by A13,NAT_1:12;
          then x0-r1<(seq^\k).n by NAT_1:def 3;
          then x in {g1: x0-r1<g1 & g1<x0} by A17,A18;
          hence x in ].x0-r1,x0.[ by RCOMP_1:def 2;
        end;
        then
A19:    rng(seq^\k)c=].x0-r1,x0.[ by TARSKI:def 3;
        ].x0-r1,x0.[c=left_open_halfline(x0) by XXREAL_1:263;
        then
A20:    rng(seq^\k)c=left_open_halfline(x0) by A19,XBOOLE_1:1;
A21:    dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
        then
A22:    rng seq c=dom f by A12,XBOOLE_1:1;
        then rng(seq^\k)c=dom f by A14,XBOOLE_1:1;
        then
A23:    rng(seq^\k)c=dom f/\].x0-r1,x0.[ by A19,XBOOLE_1:19;
        then
A24:    rng(seq^\k)c=dom f1/\].x0-r1,x0.[ by A8,XBOOLE_1:1;
        then
A25:    rng(seq^\k)c=dom f2/\].x0-r1,x0.[ by A8,XBOOLE_1:1;
A26:    lim(seq^\k)= x0 by A10,A11,SEQ_4:20;
A27:    dom f2/\].x0-r1,x0.[c=dom f2 by XBOOLE_1:17;
        then rng(seq^\k)c=dom f2 by A25,XBOOLE_1:1;
        then
A28:    rng(seq^\k) c=dom f2/\left_open_halfline(x0) by A20,XBOOLE_1:19;
        then
A29:    lim(f2/*(seq^\k))=lim_left(f2, x0) by A2,A10,A26,Def7;
A30:    dom f1/\].x0-r1,x0.[c=dom f1 by XBOOLE_1:17;
        then rng(seq^\k)c=dom f1 by A24,XBOOLE_1:1;
        then
A31:    rng(seq^\k)c=dom f1/\left_open_halfline(x0) by A20,XBOOLE_1:19;
        then
A32:    lim(f1/*(seq^\k))=lim_left(f1, x0) by A1,A10,A26,Def7;
A33:    now
          let n;
A34: n in NAT by ORDINAL1:def 12;
A35:      (seq^\k).n in rng(seq^\k) by VALUED_0:28;
          then f.((seq^\k).n)<=f2.((seq^\k).n) by A6,A23;
          then
A36:      (f/*(seq^\k)).n<=f2.((seq^\k).n)
by A14,A22,FUNCT_2:108,XBOOLE_1:1,A34;
          f1.((seq^\k).n)<=f.((seq^\k).n) by A6,A23,A35;
          then f1.((seq^\k).n)<=(f/*(seq^\k)).n by A14,A22,FUNCT_2:108,A34
,XBOOLE_1:1;
          hence (f1/*(seq^\k)).n<=(f/*(seq^\k)).n & (f/*(seq^\k)).n<=(f2/*(seq
          ^\k)).n by A30,A27,A24,A25,A36,FUNCT_2:108,XBOOLE_1:1,A34;
        end;
A37:    f2/*(seq^\k) is convergent by A2,A10,A26,A28;
A38:    f1/*(seq^\k) is convergent by A1,A10,A26,A31;
        then f/*(seq^\k) is convergent by A3,A32,A37,A29,A33,SEQ_2:19;
        then
A39:    (f/*seq)^\k is convergent by A12,A21,VALUED_0:27,XBOOLE_1:1;
        hence f/*seq is convergent by SEQ_4:21;
        lim(f/*(seq^\k))=lim_left(f1,x0) by A3,A38,A32,A37,A29,A33,SEQ_2:20;
        then lim((f/*seq)^\k)=lim_left(f1,x0) by A12,A21,VALUED_0:27,XBOOLE_1:1
;
        hence lim(f/*seq)=lim_left(f1,x0) by A39,SEQ_4:22;
      end;
      hence f is_left_convergent_in x0 by A4;
      hence thesis by A9,Def7;
    end;
    suppose
A40:  dom f2/\].x0-r1,x0.[c=dom f1/\].x0-r1,x0.[ & dom f/\].x0-r1,x0
      .[c=dom f2/\].x0-r1,x0.[;
A41:  now
        let seq;
        assume that
A42:    seq is convergent and
A43:    lim seq=x0 and
A44:    rng seq c= dom f/\left_open_halfline(x0);
        x0-r1<lim seq by A5,A43,Lm1;
        then consider k such that
A45:    for n st k<=n holds x0-r1<seq.n by A42,Th1;
A46:    rng(seq^\k)c=rng seq by VALUED_0:21;
        dom f/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
        then rng seq c=left_open_halfline(x0) by A44,XBOOLE_1:1;
        then
A47:    rng(seq^\k)c=left_open_halfline(x0) by A46,XBOOLE_1:1;
        now
          let x be object;
          assume
A48:      x in rng(seq^\k);
          then consider n being Element of NAT such that
A49:      x=(seq^\k).n by FUNCT_2:113;
          (seq^\k).n in left_open_halfline(x0) by A47,A48,A49;
          then (seq^\k).n in {g: g<x0} by XXREAL_1:229;
          then
A50:      ex g st g=(seq^\k).n & g<x0;
          x0-r1<seq.(n+k) by A45,NAT_1:12;
          then x0-r1<(seq^\k).n by NAT_1:def 3;
          then x in {g1: x0-r1<g1 & g1<x0} by A49,A50;
          hence x in ].x0-r1,x0.[ by RCOMP_1:def 2;
        end;
        then
A51:    rng(seq^\k)c=].x0-r1,x0.[ by TARSKI:def 3;
        ].x0-r1,x0.[c=left_open_halfline(x0) by XXREAL_1:263;
        then
A52:    rng(seq^\k)c=left_open_halfline(x0) by A51,XBOOLE_1:1;
A53:    dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
        then
A54:    rng seq c=dom f by A44,XBOOLE_1:1;
        then rng(seq^\k)c=dom f by A46,XBOOLE_1:1;
        then
A55:    rng(seq^\k)c=dom f/\].x0-r1,x0.[ by A51,XBOOLE_1:19;
        then
A56:    rng(seq^\k)c=dom f2/\].x0-r1,x0.[ by A40,XBOOLE_1:1;
        then
A57:    rng(seq^\k)c=dom f1/\].x0-r1,x0.[ by A40,XBOOLE_1:1;
A58:    lim(seq^\k)= x0 by A42,A43,SEQ_4:20;
A59:    dom f2/\].x0-r1,x0.[c=dom f2 by XBOOLE_1:17;
        then rng(seq^\k)c=dom f2 by A56,XBOOLE_1:1;
        then
A60:    rng(seq^\k)c=dom f2/\left_open_halfline(x0) by A52,XBOOLE_1:19;
        then
A61:    lim(f2/*(seq^\k))=lim_left(f2, x0) by A2,A42,A58,Def7;
A62:    dom f1/\].x0-r1,x0.[c=dom f1 by XBOOLE_1:17;
        then rng(seq^\k)c=dom f1 by A57,XBOOLE_1:1;
        then
A63:    rng(seq^\k)c=dom f1/\left_open_halfline(x0) by A52,XBOOLE_1:19;
        then
A64:    lim(f1/*(seq^\k))=lim_left(f1, x0) by A1,A42,A58,Def7;
A65:    now
          let n;
A66: n in NAT by ORDINAL1:def 12;
A67:      (seq^\k).n in rng(seq^\k) by VALUED_0:28;
          then f.((seq^\k).n)<=f2.((seq^\k).n) by A6,A55;
          then
A68:      (f/*(seq^\k)).n<=f2.((seq^\k).n)
by A46,A54,FUNCT_2:108,XBOOLE_1:1,A66;
          f1.((seq^\k).n)<=f.((seq^\k).n) by A6,A55,A67;
          then f1.((seq^\k).n)<=(f/*(seq^\k)).n by A46,A54,FUNCT_2:108,A66
,XBOOLE_1:1;
          hence (f1/*(seq^\k)).n<=(f/*(seq^\k)).n & (f/*(seq^\k)).n<=(f2/*(seq
          ^\k)).n by A62,A59,A56,A57,A68,FUNCT_2:108,XBOOLE_1:1,A66;
        end;
A69:    f2/*(seq^\k) is convergent by A2,A42,A58,A60;
A70:    f1/*(seq^\k) is convergent by A1,A42,A58,A63;
        then f/*(seq^\k) is convergent by A3,A64,A69,A61,A65,SEQ_2:19;
        then
A71:    (f/*seq)^\k is convergent by A44,A53,VALUED_0:27,XBOOLE_1:1;
        hence f/*seq is convergent by SEQ_4:21;
        lim(f/*(seq^\k))=lim_left(f1,x0) by A3,A70,A64,A69,A61,A65,SEQ_2:20;
        then lim((f/*seq)^\k)=lim_left(f1,x0) by A44,A53,VALUED_0:27,XBOOLE_1:1
;
        hence lim(f/*seq)=lim_left(f1,x0) by A71,SEQ_4:22;
      end;
      hence f is_left_convergent_in x0 by A4;
      hence thesis by A41,Def7;
    end;
  end;
  hence thesis;
end;

theorem
  f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left(
f1,x0)=lim_left(f2,x0) & (ex r st 0<r & ].x0-r,x0.[ c= dom f1 /\ dom f2 /\ dom
  f & for g st g in ].x0-r,x0.[ holds f1.g<=f.g & f.g<=f2.g) implies f
  is_left_convergent_in x0 & lim_left(f,x0)=lim_left(f1,x0)
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_left_convergent_in x0 and
A3: lim_left(f1,x0)=lim_left(f2,x0);
  given r such that
A4: 0<r and
A5: ].x0-r,x0.[c=dom f1/\dom f2/\dom f and
A6: for g st g in ].x0-r,x0.[ holds f1.g<=f.g & f.g<=f2.g;
  dom f1/\dom f2/\dom f c=dom f1/\dom f2 by XBOOLE_1:17;
  then
A7: ].x0-r,x0.[c=dom f1/\dom f2 by A5,XBOOLE_1:1;
A8: dom f1/\dom f2/\dom f c=dom f by XBOOLE_1:17;
  then
A9: ].x0-r,x0.[c=dom f by A5,XBOOLE_1:1;
A10: now
    let r1 such that
A11: r1<x0;
    now
      per cases;
      suppose
A12:    r1<=x0-r;
        now
          x0-r<x0 by A4,Lm1;
          then consider g being Real such that
A13:      x0-r<g and
A14:      g<x0 by XREAL_1:5;
          reconsider g as Real;
          take g;
          thus r1<g & g<x0 by A12,A13,A14,XXREAL_0:2;
          g in {g2: x0-r<g2 & g2<x0} by A13,A14;
          then g in ].x0-r,x0.[ by RCOMP_1:def 2;
          hence g in dom f by A9;
        end;
        hence ex g st r1<g & g<x0 & g in dom f;
      end;
      suppose
A15:    x0-r<=r1;
        now
          consider g being Real such that
A16:      r1<g and
A17:      g<x0 by A11,XREAL_1:5;
          reconsider g as Real;
          take g;
          thus r1<g & g<x0 by A16,A17;
          x0-r<g by A15,A16,XXREAL_0:2;
          then g in {g2: x0-r<g2 & g2<x0} by A17;
          then g in ].x0-r,x0.[ by RCOMP_1:def 2;
          hence g in dom f by A9;
        end;
        hence ex g st r1<g & g<x0 & g in dom f;
      end;
    end;
    hence ex g st r1<g & g<x0 & g in dom f;
  end;
  dom f1/\dom f2 c=dom f2 by XBOOLE_1:17;
  then
A18: dom f2/\].x0-r,x0.[=].x0-r,x0.[ by A7,XBOOLE_1:1,28;
  dom f1/\dom f2 c=dom f1 by XBOOLE_1:17;
  then
A19: dom f1/\].x0-r,x0.[=].x0-r,x0.[ by A7,XBOOLE_1:1,28;
  dom f/\].x0-r,x0.[=].x0-r,x0.[ by A5,A8,XBOOLE_1:1,28;
  hence thesis by A1,A2,A3,A4,A6,A19,A18,A10,Th63;
end;

theorem Th65:
  f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
  lim_right(f1,x0)=lim_right(f2,x0) & (for r st x0<r ex g st g<r & x0<g & g in
dom f) & (ex r st 0<r & (for g st g in dom f /\ ].x0,x0+r.[ holds f1.g<=f.g & f
.g<=f2.g) & ((dom f1 /\ ].x0,x0+r.[ c= dom f2 /\ ].x0,x0+r.[ & dom f /\ ].x0,x0
+r.[ c= dom f1 /\ ].x0,x0+r.[) or (dom f2 /\ ].x0,x0+r.[ c= dom f1 /\ ].x0,x0+r
  .[ & dom f /\ ].x0,x0+r.[ c= dom f2 /\ ].x0,x0+r.[))) implies f
  is_right_convergent_in x0 & lim_right(f,x0)=lim_right(f1,x0)
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_right_convergent_in x0 and
A3: lim_right(f1,x0)=lim_right(f2,x0) and
A4: for r st x0<r ex g st g<r & x0<g & g in dom f;
  given r1 such that
A5: 0<r1 and
A6: for g st g in dom f/\].x0,x0+r1.[ holds f1.g<=f.g & f.g<=f2.g and
A7: dom f1/\].x0,x0+r1.[c=dom f2/\].x0,x0+r1.[ & dom f/\].x0,x0+r1.[c=
dom f1/\].x0,x0+r1.[ or dom f2/\].x0,x0+r1.[c=dom f1/\].x0,x0+r1.[ & dom f/\].
  x0,x0+r1.[c=dom f2/\].x0,x0+r1.[;
  now
    per cases by A7;
    suppose
A8:   dom f1/\].x0,x0+r1.[c=dom f2/\].x0,x0+r1.[ & dom f/\].x0,x0+r1.[
      c=dom f1/\].x0,x0+r1.[;
A9:   now
        let seq;
        assume that
A10:    seq is convergent and
A11:    lim seq=x0 and
A12:    rng seq c=dom f/\right_open_halfline(x0);
        x0<lim seq+r1 by A5,A11,Lm1;
        then consider k such that
A13:    for n st k<=n holds seq.n<x0+r1 by A10,A11,Th2;
A14:    rng(seq^\k)c=rng seq by VALUED_0:21;
        dom f/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
        then rng seq c=right_open_halfline(x0) by A12,XBOOLE_1:1;
        then
A15:    rng(seq^\k)c=right_open_halfline(x0) by A14,XBOOLE_1:1;
        now
          let x be object;
          assume
A16:      x in rng(seq^\k);
          then consider n being Element of NAT such that
A17:      x=(seq^\k).n by FUNCT_2:113;
          (seq^\k).n in right_open_halfline(x0) by A15,A16,A17;
          then (seq^\k).n in {g: x0<g} by XXREAL_1:230;
          then
A18:      ex g st g=(seq^\k).n & x0<g;
          seq.(n+k)<x0+r1 by A13,NAT_1:12;
          then (seq^\k).n<x0+r1 by NAT_1:def 3;
          then x in {g1: x0<g1 & g1<x0+r1} by A17,A18;
          hence x in ].x0,x0+r1.[ by RCOMP_1:def 2;
        end;
        then
A19:    rng(seq^\k)c=].x0,x0+r1.[ by TARSKI:def 3;
        ].x0,x0+r1.[c=right_open_halfline(x0) by XXREAL_1:247;
        then
A20:    rng(seq^\k)c=right_open_halfline(x0) by A19,XBOOLE_1:1;
A21:    dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
        then
A22:    rng seq c=dom f by A12,XBOOLE_1:1;
        then rng(seq^\k)c=dom f by A14,XBOOLE_1:1;
        then
A23:    rng(seq^\k)c=dom f/\].x0,x0+r1.[ by A19,XBOOLE_1:19;
        then
A24:    rng(seq^\k)c=dom f1/\].x0,x0+r1.[ by A8,XBOOLE_1:1;
        then
A25:    rng(seq^\k)c=dom f2/\].x0,x0+r1.[ by A8,XBOOLE_1:1;
A26:    lim(seq^\k)= x0 by A10,A11,SEQ_4:20;
A27:    dom f2/\].x0,x0+r1.[c=dom f2 by XBOOLE_1:17;
        then rng(seq^\k)c=dom f2 by A25,XBOOLE_1:1;
        then
A28:    rng(seq^\k)c=dom f2/\right_open_halfline(x0) by A20,XBOOLE_1:19;
        then
A29:    lim(f2/*(seq^\k))=lim_right(f2, x0) by A2,A10,A26,Def8;
A30:    dom f1/\].x0,x0+r1.[c=dom f1 by XBOOLE_1:17;
        then rng(seq^\k)c=dom f1 by A24,XBOOLE_1:1;
        then
A31:    rng(seq^\k)c=dom f1/\right_open_halfline(x0) by A20,XBOOLE_1:19;
        then
A32:    lim(f1/*(seq^\k))=lim_right(f1, x0) by A1,A10,A26,Def8;
A33:    now
          let n;
A34: n in NAT by ORDINAL1:def 12;
A35:      (seq^\k).n in rng(seq^\k) by VALUED_0:28;
          then f.((seq^\k).n)<=f2.((seq^\k).n) by A6,A23;
          then
A36:      (f/*(seq^\k)).n<=f2.((seq^\k).n)
by A14,A22,FUNCT_2:108,XBOOLE_1:1,A34;
          f1.((seq^\k).n)<=f.((seq^\k).n) by A6,A23,A35;
          then f1.((seq^\k).n)<=(f/*(seq^\k)).n by A14,A22,FUNCT_2:108,A34
,XBOOLE_1:1;
          hence (f1/*(seq^\k)).n<=(f/*(seq^\k)).n & (f/*(seq^\k)).n<=(f2/*(seq
          ^\k)).n by A30,A27,A24,A25,A36,FUNCT_2:108,XBOOLE_1:1,A34;
        end;
A37:    f2/*(seq^\k) is convergent by A2,A10,A26,A28;
A38:    f1/*(seq^\k) is convergent by A1,A10,A26,A31;
        then f/*(seq^\k) is convergent by A3,A32,A37,A29,A33,SEQ_2:19;
        then
A39:    (f/*seq)^\k is convergent by A12,A21,VALUED_0:27,XBOOLE_1:1;
        hence f/*seq is convergent by SEQ_4:21;
        lim(f/*(seq^\k))=lim_right(f1,x0) by A3,A38,A32,A37,A29,A33,SEQ_2:20;
        then lim((f/*seq)^\k)=lim_right(f1,x0 ) by A12,A21,VALUED_0:27
,XBOOLE_1:1;
        hence lim(f/*seq)=lim_right(f1,x0) by A39,SEQ_4:22;
      end;
      hence f is_right_convergent_in x0 by A4;
      hence thesis by A9,Def8;
    end;
    suppose
A40:  dom f2/\].x0,x0+r1.[c=dom f1/\].x0,x0+r1.[ & dom f/\].x0,x0+r1
      .[ c=dom f2/\].x0,x0+r1.[;
A41:  now
        let seq;
        assume that
A42:    seq is convergent and
A43:    lim seq=x0 and
A44:    rng seq c= dom f/\right_open_halfline(x0);
        x0<lim seq+r1 by A5,A43,Lm1;
        then consider k such that
A45:    for n st k<=n holds seq.n<x0+r1 by A42,A43,Th2;
A46:    rng(seq^\k)c=rng seq by VALUED_0:21;
        dom f/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
        then rng seq c=right_open_halfline(x0) by A44,XBOOLE_1:1;
        then
A47:    rng(seq^\k)c=right_open_halfline(x0) by A46,XBOOLE_1:1;
        now
          let x be object;
          assume
A48:      x in rng(seq^\k);
          then consider n being Element of NAT such that
A49:      x=(seq^\k).n by FUNCT_2:113;
          (seq^\k).n in right_open_halfline(x0) by A47,A48,A49;
          then (seq^\k).n in {g: x0<g} by XXREAL_1:230;
          then
A50:      ex g st g=(seq^\k).n & x0<g;
          seq.(n+k)<x0+r1 by A45,NAT_1:12;
          then (seq^\k).n<x0+r1 by NAT_1:def 3;
          then x in {g1: x0<g1 & g1<x0+r1} by A49,A50;
          hence x in ].x0,x0+r1.[ by RCOMP_1:def 2;
        end;
        then
A51:    rng(seq^\k)c=].x0,x0+r1.[ by TARSKI:def 3;
        ].x0,x0+r1.[c=right_open_halfline(x0) by XXREAL_1:247;
        then
A52:    rng(seq^\k)c=right_open_halfline(x0) by A51,XBOOLE_1:1;
A53:    dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
        then
A54:    rng seq c=dom f by A44,XBOOLE_1:1;
        then rng(seq^\k)c=dom f by A46,XBOOLE_1:1;
        then
A55:    rng(seq^\k)c=dom f/\].x0,x0+r1.[ by A51,XBOOLE_1:19;
        then
A56:    rng(seq^\k)c=dom f2/\].x0,x0+r1.[ by A40,XBOOLE_1:1;
        then
A57:    rng(seq^\k)c=dom f1/\].x0,x0+r1.[ by A40,XBOOLE_1:1;
A58:    lim(seq^\k)= x0 by A42,A43,SEQ_4:20;
A59:    dom f2/\].x0,x0+r1.[c=dom f2 by XBOOLE_1:17;
        then rng(seq^\k)c=dom f2 by A56,XBOOLE_1:1;
        then
A60:    rng(seq^\k)c=dom f2/\right_open_halfline(x0) by A52,XBOOLE_1:19;
        then
A61:    lim(f2/*(seq^\k))=lim_right(f2, x0) by A2,A42,A58,Def8;
A62:    dom f1/\].x0,x0+r1.[c=dom f1 by XBOOLE_1:17;
        then rng(seq^\k)c=dom f1 by A57,XBOOLE_1:1;
        then
A63:    rng(seq^\k)c=dom f1/\right_open_halfline(x0) by A52,XBOOLE_1:19;
        then
A64:    lim(f1/*(seq^\k))=lim_right(f1, x0) by A1,A42,A58,Def8;
A65:    now
          let n;
A66: n in NAT by ORDINAL1:def 12;
A67:      (seq^\k).n in rng(seq^\k) by VALUED_0:28;
          then f.((seq^\k).n)<=f2.((seq^\k).n) by A6,A55;
          then
A68:      (f/*(seq^\k)).n<=f2.((seq^\k).n)
by A46,A54,FUNCT_2:108,XBOOLE_1:1,A66;
          f1.((seq^\k).n)<=f.((seq^\k).n) by A6,A55,A67;
          then f1.((seq^\k).n)<=(f/*(seq^\k)).n by A46,A54,FUNCT_2:108,A66
,XBOOLE_1:1;
          hence (f1/*(seq^\k)).n<=(f/*(seq^\k)).n & (f/*(seq^\k)).n<=(f2/*(seq
          ^\k)).n by A62,A59,A56,A57,A68,FUNCT_2:108,XBOOLE_1:1,A66;
        end;
A69:    f2/*(seq^\k) is convergent by A2,A42,A58,A60;
A70:    f1/*(seq^\k) is convergent by A1,A42,A58,A63;
        then f/*(seq^\k) is convergent by A3,A64,A69,A61,A65,SEQ_2:19;
        then
A71:    (f/*seq)^\k is convergent by A44,A53,VALUED_0:27,XBOOLE_1:1;
        hence f/*seq is convergent by SEQ_4:21;
        lim(f/*(seq^\k))=lim_right(f1,x0) by A3,A70,A64,A69,A61,A65,SEQ_2:20;
        then lim((f/*seq)^\k)=lim_right(f1,x0 ) by A44,A53,VALUED_0:27
,XBOOLE_1:1;
        hence lim(f/*seq)=lim_right(f1,x0) by A71,SEQ_4:22;
      end;
      hence f is_right_convergent_in x0 by A4;
      hence thesis by A41,Def8;
    end;
  end;
  hence thesis;
end;

theorem
  f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
lim_right(f1,x0)=lim_right(f2,x0) & (ex r st 0<r & ].x0,x0+r.[ c= dom f1 /\ dom
f2 /\ dom f & for g st g in ].x0,x0+r.[ holds f1.g<=f.g & f.g<=f2.g) implies f
  is_right_convergent_in x0 & lim_right(f,x0)=lim_right(f1,x0)
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_right_convergent_in x0 and
A3: lim_right(f1,x0)=lim_right(f2,x0);
  given r such that
A4: 0<r and
A5: ].x0,x0+r.[c=dom f1/\dom f2/\dom f and
A6: for g st g in ].x0,x0+r.[ holds f1.g<=f.g & f.g<=f2.g;
  dom f1/\dom f2/\dom f c=dom f1/\dom f2 by XBOOLE_1:17;
  then
A7: ].x0,x0+r.[c=dom f1/\dom f2 by A5,XBOOLE_1:1;
A8: dom f1/\dom f2/\dom f c=dom f by XBOOLE_1:17;
  then
A9: ].x0,x0+r.[c=dom f by A5,XBOOLE_1:1;
A10: now
    let r1 such that
A11: x0<r1;
    now
      per cases;
      suppose
A12:    r1<=x0+r;
        now
          consider g being Real such that
A13:      x0<g and
A14:      g<r1 by A11,XREAL_1:5;
          reconsider g as Real;
          take g;
          thus g<r1 & x0<g by A13,A14;
          g<x0+r by A12,A14,XXREAL_0:2;
          then g in {g2: x0<g2 & g2<x0+r} by A13;
          then g in ].x0,x0+r.[ by RCOMP_1:def 2;
          hence g in dom f by A9;
        end;
        hence ex g st g<r1 & x0<g & g in dom f;
      end;
      suppose
A15:    x0+r<=r1;
        now
          x0+0<x0+r by A4,XREAL_1:8;
          then consider g being Real such that
A16:      x0<g and
A17:      g<x0+r by XREAL_1:5;
          reconsider g as Real;
          take g;
          thus g<r1 & x0<g by A15,A16,A17,XXREAL_0:2;
          g in {g2: x0<g2 & g2<x0+r} by A16,A17;
          then g in ].x0,x0+r.[ by RCOMP_1:def 2;
          hence g in dom f by A9;
        end;
        hence ex g st g<r1 & x0<g & g in dom f;
      end;
    end;
    hence ex g st g<r1 & x0<g & g in dom f;
  end;
  dom f1/\dom f2 c=dom f2 by XBOOLE_1:17;
  then
A18: dom f2/\].x0,x0+r.[=].x0,x0+r.[ by A7,XBOOLE_1:1,28;
  dom f1/\dom f2 c=dom f1 by XBOOLE_1:17;
  then
A19: dom f1/\].x0,x0+r.[=].x0,x0+r.[ by A7,XBOOLE_1:1,28;
  dom f/\].x0,x0+r.[=].x0,x0+r.[ by A5,A8,XBOOLE_1:1,28;
  hence thesis by A1,A2,A3,A4,A6,A19,A18,A10,Th65;
end;

theorem
  f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & (ex r st 0
<r & ((dom f1 /\ ].x0-r,x0.[ c= dom f2 /\ ].x0-r,x0.[ & for g st g in dom f1 /\
].x0-r,x0.[ holds f1.g<=f2.g) or (dom f2 /\ ].x0-r,x0.[ c= dom f1 /\ ].x0-r,x0
.[ & for g st g in dom f2 /\ ].x0-r,x0.[ holds f1.g<=f2.g))) implies lim_left(
  f1,x0)<=lim_left(f2,x0)
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_left_convergent_in x0;
  given r such that
A3: 0<r and
A4: (dom f1/\].x0-r,x0.[c=dom f2/\].x0-r,x0.[ & for g st g in dom f1/\].
x0-r,x0.[ holds f1.g<=f2.g) or (dom f2/\].x0-r,x0.[c=dom f1/\].x0-r,x0.[ & for
  g st g in dom f2/\].x0-r,x0.[ holds f1.g<=f2.g);
  now
    per cases by A4;
    suppose
A5:   dom f1/\].x0-r,x0.[c=dom f2/\].x0-r,x0.[ & for g st g in dom f1
      /\].x0-r,x0.[ 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;
        x0-1/(n+1)<x0 by Lm3;
        then consider g such that
A7:     x0-1/(n+1)<g and
A8:    g<x0 and
A9:    g in dom f1 by A1;
         reconsider g as Element of REAL by XREAL_0:def 1;
        take g;
        thus X[n,g] by A7,A8,A9;
      end;
      consider s be Real_Sequence such that
A10:  for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A6);
A11: for n being Nat holds X[n,s.n]
     proof let n be Nat;
      n in NAT by ORDINAL1:def 12;
      hence thesis by A10;
     end;
A12:  lim s=x0 by A11,Th5;
A13:  rng s c=dom f1/\left_open_halfline(x0) by A11,Th5;
A14:  ].x0-r,x0.[c=left_open_halfline(x0) by XXREAL_1:263;
A15:  s is convergent by A11,Th5;
      x0-r<x0 by A3,Lm1;
      then consider k such that
A16:  for n st k<=n holds x0-r<s.n by A15,A12,Th1;
A17:  lim(s^\k)=x0 by A15,A12,SEQ_4:20;
      now
        let x be object;
        assume x in rng(s^\k);
        then consider n being Element of NAT such that
A18:    (s^\k).n=x by FUNCT_2:113;
        s.(n+k)<x0 by A11;
        then
A19:    (s^\k).n<x0 by NAT_1:def 3;
        s.(n+k) in dom f1 by A11;
        then
A20:    (s^\k).n in dom f1 by NAT_1:def 3;
        x0-r<s.(n+k) by A16,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 A19;
        then (s^\k).n in ].x0-r,x0 .[ by RCOMP_1:def 2;
        hence x in dom f1/\].x0-r,x0.[ by A18,A20,XBOOLE_0:def 4;
      end;
      then
A21:  rng(s^\k)c=dom f1/\].x0-r,x0.[ by TARSKI:def 3;
      then
A22:  rng(s^\k)c=dom f2/\].x0-r,x0.[ by A5,XBOOLE_1:1;
      dom f2/\ ].x0-r,x0.[c=].x0-r,x0.[ by XBOOLE_1:17;
      then rng(s^\k)c=].x0-r,x0.[ by A22,XBOOLE_1:1;
      then
A23:  rng(s^\k)c=left_open_halfline(x0) by A14,XBOOLE_1:1;
A24:  dom f2/\].x0-r,x0.[c=dom f2 by XBOOLE_1:17;
      then rng(s^\k)c=dom f2 by A22,XBOOLE_1:1;
      then
A25:  rng(s^\k)c=dom f2/\left_open_halfline(x0) by A23,XBOOLE_1:19;
      then
A26:  lim(f2/*(s^\k))=lim_left(f2,x0) by A2,A15,A17,Def7;
      rng(s^\k)c=rng s by VALUED_0:21;
      then
A27:  rng(s^\k)c=dom f1/\left_open_halfline(x0) by A13,XBOOLE_1:1;
      then
A28:  lim(f1/*(s^\k))=lim_left(f1,x0) by A1,A15,A17,Def7;
A29:  dom f1/\].x0-r,x0.[c=dom f1 by XBOOLE_1:17;
A30:  now
        let n;
A31: 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,A21;
        then f1.((s^\k).n)<=(f2/*(s^\k)).n
by A22,A24,FUNCT_2:108,XBOOLE_1:1,A31;
        hence (f1/*(s^\k)).n<=(f2/*(s^\k)).n
by A21,A29,FUNCT_2:108,XBOOLE_1:1,A31;
      end;
A32:  f2/*(s^\k) is convergent by A2,A15,A17,A25;
      f1/*(s^\k) is convergent by A1,A15,A17,A27;
      hence thesis by A28,A32,A26,A30,SEQ_2:18;
    end;
    suppose
A33:  dom f2/\].x0-r,x0.[c=dom f1/\].x0-r,x0.[ & for g st g in dom f2
      /\].x0-r,x0.[ holds f1.g<=f2.g;
      defpred X[Nat,Real] means x0-1/($1+1)<$2 & $2<x0 & $2
      in dom f2;
A34:  now
        let n be Element of NAT;
        0<1/(n+1) by XREAL_1:139;
        then x0-1/(n+1)<x0-0 by XREAL_1:15;
        then consider g such that
A35:    x0-1/(n+1)<g and
A36:    g<x0 and
A37:    g in dom f2 by A2;
         reconsider g as Element of REAL by XREAL_0:def 1;
        take g;
        thus X[n,g] by A35,A36,A37;
      end;
      consider s be Real_Sequence such that
A38:  for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A34 );
A39: for n being Nat holds X[n,s.n]
     proof let n be Nat;
      n in NAT by ORDINAL1:def 12;
      hence thesis by A38;
     end;
A40:  lim s=x0 by A39,Th5;
A41:  rng s c=dom f2/\left_open_halfline(x0) by A39,Th5;
A42:  ].x0-r,x0.[c=left_open_halfline(x0) by XXREAL_1:263;
A43:  s is convergent by A39,Th5;
      x0-r<x0 by A3,Lm1;
      then consider k such that
A44:  for n st k<=n holds x0-r<s.n by A43,A40,Th1;
A45:  lim(s^\k)=x0 by A43,A40,SEQ_4:20;
A46:  now
        let x be object;
        assume x in rng(s^\k);
        then consider n being Element of NAT such that
A47:    (s^\k).n=x by FUNCT_2:113;
        s.(n+k)<x0 by A39;
        then
A48:    (s^\k).n<x0 by NAT_1:def 3;
        s.(n+k) in dom f2 by A39;
        then
A49:    (s^\k).n in dom f2 by NAT_1:def 3;
        x0-r<s.(n+k) by A44,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 A48;
        then (s^\k).n in ].x0-r,x0 .[ by RCOMP_1:def 2;
        hence x in dom f2/\].x0-r,x0.[ by A47,A49,XBOOLE_0:def 4;
      end;
      then
A50:  rng(s^\k)c=dom f2/\].x0-r,x0.[ by TARSKI:def 3;
      then
A51:  rng(s^\k)c=dom f1/\].x0-r,x0.[ by A33,XBOOLE_1:1;
      dom f1/\ ].x0-r,x0.[c=].x0-r,x0.[ by XBOOLE_1:17;
      then rng(s^\k)c=].x0-r,x0.[ by A51,XBOOLE_1:1;
      then
A52:  rng(s^\k)c=left_open_halfline(x0) by A42,XBOOLE_1:1;
A53:  dom f1/\].x0-r,x0.[c=dom f1 by XBOOLE_1:17;
      then rng(s^\k)c=dom f1 by A51,XBOOLE_1:1;
      then
A54:  rng(s^\k)c=dom f1/\left_open_halfline(x0) by A52,XBOOLE_1:19;
      then
A55:  lim(f1/*(s^\k))=lim_left(f1,x0) by A1,A43,A45,Def7;
      rng(s^\k)c=rng s by VALUED_0:21;
      then
A56:  rng(s^\k)c=dom f2/\left_open_halfline(x0) by A41,XBOOLE_1:1;
      then
A57:  lim(f2/*(s^\k))=lim_left(f2,x0) by A2,A43,A45,Def7;
A58:  dom f2/\].x0-r,x0.[c=dom f2 by XBOOLE_1:17;
A59:  now
        let n;
A60: 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 A33,A46;
        then f1.((s^\k).n)<=(f2/*(s^\k)).n
by A50,A58,FUNCT_2:108,XBOOLE_1:1,A60;
        hence (f1/*(s^\k)).n<=(f2/*(s^\k)).n
by A51,A53,FUNCT_2:108,XBOOLE_1:1,A60;
      end;
A61:  f1/*(s^\k) is convergent by A1,A43,A45,A54;
      f2/*(s^\k) is convergent by A2,A43,A45,A56;
      hence thesis by A57,A61,A55,A59,SEQ_2:18;
    end;
  end;
  hence thesis;
end;

theorem
  f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & (ex r st
  0<r & ((dom f1 /\ ].x0,x0+r.[ c= dom f2 /\ ].x0,x0+r.[ & for g st g in dom f1
/\ ].x0,x0+r.[ holds f1.g<=f2.g) or (dom f2 /\ ].x0,x0+r.[ c= dom f1 /\ ].x0,x0
  +r.[ & for g st g in dom f2 /\ ].x0,x0+r.[ holds f1.g<=f2.g))) implies
  lim_right(f1,x0)<=lim_right(f2,x0)
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_right_convergent_in x0;
  given r such that
A3: 0<r and
A4: (dom f1/\].x0,x0+r.[c=dom f2/\].x0,x0+r.[ & for g st g in dom f1/\].
x0,x0+r.[ holds f1.g<=f2.g) or (dom f2/\].x0,x0+r.[c=dom f1/\].x0,x0+r.[ & for
  g st g in dom f2/\].x0,x0+r.[ holds f1.g<=f2.g);
  now
    per cases by A4;
    suppose
A5:   dom f1/\].x0,x0+r.[c=dom f2/\].x0,x0+r.[ & for g st g in dom f1
      /\].x0,x0+r.[ holds f1.g<=f2.g;
      defpred X[Nat,Real] means x0<$2 & $2<x0+1/($1+1) & $2
      in dom f1;
A6:   now
        let n be Element of NAT;
        x0<x0+1/(n+1) by Lm3;
        then consider g such that
A7:     g<x0+(1/(n+1)) and
A8:    x0<g and
A9:    g in dom f1 by A1;
         reconsider g as Element of REAL by XREAL_0:def 1;
        take g;
        thus X[n,g] by A7,A8,A9;
      end;
      consider s be Real_Sequence such that
A10:  for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A6);
A11: for n being Nat holds X[n,s.n]
     proof let n be Nat;
      n in NAT by ORDINAL1:def 12;
      hence thesis by A10;
     end;
A12:  lim s=x0 by A11,Th6;
A13:  rng s c=dom f1/\right_open_halfline(x0) by A11,Th6;
A14:  ].x0,x0+r.[c=right_open_halfline(x0) by XXREAL_1:247;
A15:  s is convergent by A11,Th6;
      x0<x0+r by A3,Lm1;
      then consider k such that
A16:  for n st k<=n holds s.n<x0+r by A15,A12,Th2;
A17:  lim(s^\k)=x0 by A15,A12,SEQ_4:20;
      now
        let x be object;
        assume x in rng(s^\k);
        then consider n being Element of NAT such that
A18:    (s^\k).n=x by FUNCT_2:113;
        x0<s.(n+k) by A11;
        then
A19:    x0<(s^\k).n by NAT_1:def 3;
        s.(n+k) in dom f1 by A11;
        then
A20:    (s^\k).n in dom f1 by NAT_1:def 3;
        s.(n+k)<x0+r by A16,NAT_1:12;
        then (s^\k).n<x0+r by NAT_1:def 3;
        then (s^\k).n in {g2: x0<g2 & g2<x0+r} by A19;
        then (s^\k).n in ].x0,x0+r .[ by RCOMP_1:def 2;
        hence x in dom f1/\].x0,x0+r.[ by A18,A20,XBOOLE_0:def 4;
      end;
      then
A21:  rng(s^\k)c=dom f1/\].x0,x0+r.[ by TARSKI:def 3;
      then
A22:  rng(s^\k)c=dom f2/\].x0,x0+r.[ by A5,XBOOLE_1:1;
      dom f2/\ ].x0,x0+r.[c=].x0,x0+r.[ by XBOOLE_1:17;
      then rng(s^\k)c=].x0,x0+r.[ by A22,XBOOLE_1:1;
      then
A23:  rng(s^\k)c=right_open_halfline(x0) by A14,XBOOLE_1:1;
A24:  dom f2/\].x0,x0+r.[c=dom f2 by XBOOLE_1:17;
      then rng(s^\k)c=dom f2 by A22,XBOOLE_1:1;
      then
A25:  rng(s^\k)c=dom f2/\right_open_halfline(x0) by A23,XBOOLE_1:19;
      then
A26:  lim(f2/*(s^\k))=lim_right(f2,x0) by A2,A15,A17,Def8;
      rng(s^\k)c=rng s by VALUED_0:21;
      then
A27:  rng(s^\k)c=dom f1/\right_open_halfline(x0) by A13,XBOOLE_1:1;
      then
A28:  lim(f1/*(s^\k))=lim_right(f1,x0) by A1,A15,A17,Def8;
A29:  dom f1/\].x0,x0+r.[c=dom f1 by XBOOLE_1:17;
A30:  now
        let n;
A31: 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,A21;
        then f1.((s^\k).n)<=(f2/*(s^\k)).n
by A22,A24,FUNCT_2:108,XBOOLE_1:1,A31;
        hence (f1/*(s^\k)).n<=(f2/*(s^\k)).n
by A21,A29,FUNCT_2:108,XBOOLE_1:1,A31;
      end;
A32:  f2/*(s^\k) is convergent by A2,A15,A17,A25;
      f1/*(s^\k) is convergent by A1,A15,A17,A27;
      hence thesis by A28,A32,A26,A30,SEQ_2:18;
    end;
    suppose
A33:  dom f2/\].x0,x0+r.[c=dom f1/\].x0,x0+r.[ & for g st g in dom f2
      /\].x0,x0+r.[ holds f1.g<=f2.g;
      defpred X[Nat,Real] means x0<$2 & $2<x0+1/($1+1) & $2
      in dom f2;
A34:  now
        let n be Element of NAT;
        0<1/(n+1) by XREAL_1:139;
        then x0+0<x0+1/(n+1) by XREAL_1:8;
        then consider g such that
A35:    g<x0+(1/(n+1)) and
A36:    x0<g and
A37:    g in dom f2 by A2;
         reconsider g as Element of REAL by XREAL_0:def 1;
        take g;
        thus X[n,g] by A35,A36,A37;
      end;
      consider s be Real_Sequence such that
A38:  for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A34);
A39: for n being Nat holds X[n,s.n]
     proof let n be Nat;
      n in NAT by ORDINAL1:def 12;
      hence thesis by A38;
     end;
A40:  lim s=x0 by A39,Th6;
A41:  rng s c=dom f2/\right_open_halfline(x0) by A39,Th6;
A42:  ].x0,x0+r.[c=right_open_halfline(x0) by XXREAL_1:247;
A43:  s is convergent by A39,Th6;
      x0<x0+r by A3,Lm1;
      then consider k such that
A44:  for n st k<=n holds s.n<x0+r by A43,A40,Th2;
A45:  lim(s^\k)=x0 by A43,A40,SEQ_4:20;
A46:  now
        let x be object;
        assume x in rng(s^\k);
        then consider n being Element of NAT such that
A47:    (s^\k).n=x by FUNCT_2:113;
        x0<s.(n+k) by A39;
        then
A48:    x0<(s^\k).n by NAT_1:def 3;
        s.(n+k) in dom f2 by A39;
        then
A49:    (s^\k).n in dom f2 by NAT_1:def 3;
        s.(n+k)<x0+r by A44,NAT_1:12;
        then (s^\k).n<x0+r by NAT_1:def 3;
        then (s^\k).n in {g2: x0<g2 & g2<x0+r} by A48;
        then (s^\k).n in ].x0,x0+r .[ by RCOMP_1:def 2;
        hence x in dom f2/\].x0,x0+r.[ by A47,A49,XBOOLE_0:def 4;
      end;
      then
A50:  rng(s^\k)c=dom f2/\].x0,x0+r.[ by TARSKI:def 3;
      then
A51:  rng(s^\k)c=dom f1/\].x0,x0+r.[ by A33,XBOOLE_1:1;
      dom f1/\ ].x0,x0+r.[c=].x0,x0+r.[ by XBOOLE_1:17;
      then rng(s^\k)c=].x0,x0+r.[ by A51,XBOOLE_1:1;
      then
A52:  rng(s^\k)c=right_open_halfline(x0) by A42,XBOOLE_1:1;
A53:  dom f1/\].x0,x0+r.[c=dom f1 by XBOOLE_1:17;
      then rng(s^\k)c=dom f1 by A51,XBOOLE_1:1;
      then
A54:  rng(s^\k)c=dom f1/\right_open_halfline(x0) by A52,XBOOLE_1:19;
      then
A55:  lim(f1/*(s^\k))=lim_right(f1,x0) by A1,A43,A45,Def8;
      rng(s^\k)c=rng s by VALUED_0:21;
      then
A56:  rng(s^\k)c=dom f2/\right_open_halfline(x0) by A41,XBOOLE_1:1;
      then
A57:  lim(f2/*(s^\k))=lim_right(f2,x0) by A2,A43,A45,Def8;
A58:  dom f2/\].x0,x0+r.[c=dom f2 by XBOOLE_1:17;
A59:  now
        let n;
A60: 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 A33,A46;
        then f1.((s^\k).n)<=(f2/*(s^\k)).n
by A50,A58,FUNCT_2:108,XBOOLE_1:1,A60;
        hence (f1/*(s^\k)).n<=(f2/*(s^\k)).n
by A51,A53,FUNCT_2:108,XBOOLE_1:1,A60;
      end;
A61:  f1/*(s^\k) is convergent by A1,A43,A45,A54;
      f2/*(s^\k) is convergent by A2,A43,A45,A56;
      hence thesis by A57,A61,A55,A59,SEQ_2:18;
    end;
  end;
  hence thesis;
end;

theorem
  (f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in
  x0) & (for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0) implies f^
  is_left_convergent_in x0 & lim_left(f^,x0)=0
proof
  assume
A1: f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0;
A2: now
    dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
    then
A3: dom(f^)c=dom f by XBOOLE_1:36;
    let seq such that
A4: seq is convergent and
A5: lim seq=x0 and
A6: rng seq c=dom(f^)/\left_open_halfline(x0);
    dom(f^)/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
    then
A7: rng seq c=left_open_halfline(x0) by A6,XBOOLE_1:1;
A8: dom(f^)/\left_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
    then rng seq c=dom(f^) by A6,XBOOLE_1:1;
    then rng seq c=dom f by A3,XBOOLE_1:1;
    then
A9: rng seq c=dom f/\left_open_halfline(x0) by A7,XBOOLE_1:19;
    now
      per cases by A1;
      suppose
        f is_left_divergent_to+infty_in x0;
        then
A10:    f/*seq is divergent_to+infty by A4,A5,A9;
        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,A8,A11,
RFUNCT_2:12,XBOOLE_1:1;
      end;
      suppose
        f is_left_divergent_to-infty_in x0;
        then
A12:    f/*seq is divergent_to-infty by A4,A5,A9;
        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,A8,A13,
RFUNCT_2:12,XBOOLE_1:1;
      end;
    end;
    hence (f^)/*seq is convergent & lim((f^)/*seq)=0;
  end;
  assume
A14: for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0;
  now
    let r;
    assume r<x0;
    then consider g such that
A15: r<g and
A16: g<x0 and
A17: g in dom f and
A18: f.g<>0 by A14;
    take g;
    thus r<g & g<x0 by A15,A16;
    not f.g in {0} by A18,TARSKI:def 1;
    then not g in f"{0} by FUNCT_1:def 7;
    then g in dom f\f"{0} by A17,XBOOLE_0:def 5;
    hence g in dom(f^) by RFUNCT_1:def 2;
  end;
  hence f^ is_left_convergent_in x0 by A2;
  hence thesis by A2,Def7;
end;

theorem
  (f is_right_divergent_to+infty_in x0 or f
is_right_divergent_to-infty_in x0 ) & (for r st x0<r ex g st g<r & x0<g & g in
  dom f & f.g<>0) implies f^ is_right_convergent_in x0 & lim_right(f^,x0)=0
proof
  assume
A1: f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0;
A2: now
    dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
    then
A3: dom(f^)c=dom f by XBOOLE_1:36;
    let seq such that
A4: seq is convergent and
A5: lim seq=x0 and
A6: rng seq c=dom(f^)/\right_open_halfline(x0);
    dom(f^)/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
    then
A7: rng seq c=right_open_halfline(x0) by A6,XBOOLE_1:1;
A8: dom(f^)/\right_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
    then rng seq c=dom(f^) by A6,XBOOLE_1:1;
    then rng seq c=dom f by A3,XBOOLE_1:1;
    then
A9: rng seq c=dom f/\right_open_halfline(x0) by A7,XBOOLE_1:19;
    now
      per cases by A1;
      suppose
        f is_right_divergent_to+infty_in x0;
        then
A10:    f/*seq is divergent_to+infty by A4,A5,A9;
        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,A8,A11,
RFUNCT_2:12,XBOOLE_1:1;
      end;
      suppose
        f is_right_divergent_to-infty_in x0;
        then
A12:    f/*seq is divergent_to-infty by A4,A5,A9;
        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,A8,A13,
RFUNCT_2:12,XBOOLE_1:1;
      end;
    end;
    hence (f^)/*seq is convergent & lim((f^)/*seq)=0;
  end;
  assume
A14: for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0;
  now
    let r;
    assume x0<r;
    then consider g such that
A15: g<r and
A16: x0<g and
A17: g in dom f and
A18: f.g<>0 by A14;
    take g;
    thus g<r & x0<g by A15,A16;
    not f.g in {0} by A18,TARSKI:def 1;
    then not g in f"{0} by FUNCT_1:def 7;
    then g in dom f\f"{0} by A17,XBOOLE_0:def 5;
    hence g in dom(f^) by RFUNCT_1:def 2;
  end;
  hence f^ is_right_convergent_in x0 by A2;
  hence thesis by A2,Def8;
end;

theorem
  f is_left_convergent_in x0 & lim_left(f,x0)=0 & (ex r st 0<r & for g
  st g in dom f /\ ].x0-r,x0.[ holds 0<f.g) implies f^
  is_left_divergent_to+infty_in x0
proof
  assume that
A1: f is_left_convergent_in x0 and
A2: lim_left(f,x0)=0;
  given r such that
A3: 0<r and
A4: for g st g in dom f/\].x0-r,x0.[ holds 0<f.g;
  thus for r1 st r1<x0 ex g1 st r1<g1 & g1<x0 & g1 in dom(f^)
  proof
    let r1;
    assume r1<x0;
    then consider g1 such that
A5: r1<g1 and
A6: g1<x0 and
    g1 in dom f by A1;
    now
      per cases;
      suppose
A7:     g1<=x0-r;
        x0-r<x0 by A3,Lm1;
        then consider g2 such that
A8:     x0-r<g2 and
A9:     g2<x0 and
A10:    g2 in dom f by A1;
        take g2;
        g1<g2 by A7,A8,XXREAL_0:2;
        hence r1<g2 & g2<x0 by A5,A9,XXREAL_0:2;
        g2 in {r2: x0-r<r2 & r2<x0} by A8,A9;
        then g2 in ].x0-r,x0.[ by RCOMP_1:def 2;
        then g2 in dom f/\].x0-r,x0.[ by A10,XBOOLE_0:def 4;
        then 0<>f.g2 by A4;
        then not f.g2 in {0} by TARSKI:def 1;
        then not g2 in f"{0} by FUNCT_1:def 7;
        then g2 in dom f\f"{0} by A10,XBOOLE_0:def 5;
        hence g2 in dom(f^) by RFUNCT_1:def 2;
      end;
      suppose
A11:    x0-r<=g1;
        consider g2 such that
A12:    g1<g2 and
A13:    g2<x0 and
A14:    g2 in dom f by A1,A6;
        take g2;
        thus r1<g2 & g2<x0 by A5,A12,A13,XXREAL_0:2;
        x0-r<g2 by A11,A12,XXREAL_0:2;
        then g2 in {r2: x0-r<r2 & r2<x0} by A13;
        then g2 in ].x0-r,x0.[ by RCOMP_1:def 2;
        then g2 in dom f/\].x0-r,x0.[ by A14,XBOOLE_0:def 4;
        then 0<>f.g2 by A4;
        then not f.g2 in {0} by TARSKI:def 1;
        then not g2 in f"{0} by FUNCT_1:def 7;
        then g2 in dom f\f"{0} by A14,XBOOLE_0:def 5;
        hence g2 in dom(f^) by RFUNCT_1:def 2;
      end;
    end;
    hence thesis;
  end;
  let s be Real_Sequence such that
A15: s is convergent and
A16: lim s=x0 and
A17: rng s c=dom(f^)/\left_open_halfline(x0);
  x0-r<x0 by A3,Lm1;
  then consider k such that
A18: for n st k<=n holds x0-r<s.n by A15,A16,Th1;
A19: lim(s^\k)=x0 by A15,A16,SEQ_4:20;
  dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
  then
A20: dom(f^)c=dom f by XBOOLE_1:36;
A21: rng(s^\k)c=rng s by VALUED_0:21;
  dom(f^)/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
  then rng s c=left_open_halfline(x0) by A17,XBOOLE_1:1;
  then
A22: rng(s^\k)c=left_open_halfline(x0) by A21,XBOOLE_1:1;
A23: dom(f^)/\left_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
  then
A24: rng s c=dom(f^) by A17,XBOOLE_1:1;
  then
A25: rng s c=dom f by A20,XBOOLE_1:1;
  then
A26: rng(s^\k)c=dom f by A21,XBOOLE_1:1;
  then
A27: rng(s^\k)c=dom f/\left_open_halfline(x0) by A22,XBOOLE_1:19;
  then
A28: lim(f/*(s^\k))=0 by A1,A2,A15,A19,Def7;
  now
    let n;
A29: n in NAT by ORDINAL1:def 12;
    x0-r<s.(n+k) by A18,NAT_1:12;
    then
A30: x0-r<(s^\k).n by NAT_1:def 3;
A31: (s^\k).n in rng(s^\k) by VALUED_0:28;
    then (s^\k).n in left_open_halfline(x0) by A22;
    then (s^\k).n in {g1: g1<x0} by XXREAL_1:229;
    then ex g1 st g1=(s^\k).n & g1<x0;
    then (s^\k).n in {g2: x0-r<g2 & g2<x0} by A30;
    then (s^\k).n in ].x0-r,x0.[ by RCOMP_1:def 2;
    then (s^\k).n in dom f/\].x0-r,x0.[ by A26,A31,XBOOLE_0:def 4;
    then 0<f.((s^\k).n) by A4;
    hence 0<(f/*(s^\k)).n by A25,A21,FUNCT_2:108,XBOOLE_1:1,A29;
  end;
  then
A32: for n holds 0<=n implies 0<(f/*(s^\k)).n;
  f/*(s^\k) is convergent by A1,A15,A19,A27;
  then
A33: (f/*(s^\k))" is divergent_to+infty by A28,A32,LIMFUNC1:35;
  (f/*(s^\k))"=((f/*s)^\k)" by A24,A20,VALUED_0:27,XBOOLE_1:1
    .=((f/*s)")^\k by SEQM_3:18
    .=((f^)/*s)^\k by A17,A23,RFUNCT_2:12,XBOOLE_1:1;
  hence thesis by A33,LIMFUNC1:7;
end;

theorem
  f is_left_convergent_in x0 & lim_left(f,x0)=0 & (ex r st 0<r & for g
  st g in dom f /\ ].x0-r,x0.[ holds f.g<0) implies f^
  is_left_divergent_to-infty_in x0
proof
  assume that
A1: f is_left_convergent_in x0 and
A2: lim_left(f,x0)=0;
  given r such that
A3: 0<r and
A4: for g st g in dom f/\].x0-r,x0.[ holds f.g<0;
  thus for r1 st r1<x0 ex g1 st r1<g1 & g1<x0 & g1 in dom(f^)
  proof
    let r1;
    assume r1<x0;
    then consider g1 such that
A5: r1<g1 and
A6: g1<x0 and
    g1 in dom f by A1;
    now
      per cases;
      suppose
A7:     g1<=x0-r;
        x0-r<x0 by A3,Lm1;
        then consider g2 such that
A8:     x0-r<g2 and
A9:     g2<x0 and
A10:    g2 in dom f by A1;
        take g2;
        g1<g2 by A7,A8,XXREAL_0:2;
        hence r1<g2 & g2<x0 by A5,A9,XXREAL_0:2;
        g2 in {r2: x0-r<r2 & r2<x0} by A8,A9;
        then g2 in ].x0-r,x0.[ by RCOMP_1:def 2;
        then g2 in dom f/\].x0-r,x0.[ by A10,XBOOLE_0:def 4;
        then not f.g2 in {0} by A4;
        then not g2 in f"{0} by FUNCT_1:def 7;
        then g2 in dom f\f"{0} by A10,XBOOLE_0:def 5;
        hence g2 in dom(f^) by RFUNCT_1:def 2;
      end;
      suppose
A11:    x0-r<=g1;
        consider g2 such that
A12:    g1<g2 and
A13:    g2<x0 and
A14:    g2 in dom f by A1,A6;
        take g2;
        thus r1<g2 & g2<x0 by A5,A12,A13,XXREAL_0:2;
        x0-r<g2 by A11,A12,XXREAL_0:2;
        then g2 in {r2: x0-r<r2 & r2<x0} by A13;
        then g2 in ].x0-r,x0.[ by RCOMP_1:def 2;
        then g2 in dom f/\].x0-r,x0.[ by A14,XBOOLE_0:def 4;
        then not f.g2 in {0} by A4;
        then not g2 in f"{0} by FUNCT_1:def 7;
        then g2 in dom f\f"{0} by A14,XBOOLE_0:def 5;
        hence g2 in dom(f^) by RFUNCT_1:def 2;
      end;
    end;
    hence thesis;
  end;
  let s be Real_Sequence such that
A15: s is convergent and
A16: lim s=x0 and
A17: rng s c=dom(f^)/\left_open_halfline(x0);
  x0-r<x0 by A3,Lm1;
  then consider k such that
A18: for n st k<=n holds x0-r<s.n by A15,A16,Th1;
A19: lim(s^\k)=x0 by A15,A16,SEQ_4:20;
  dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
  then
A20: dom(f^)c=dom f by XBOOLE_1:36;
A21: rng(s^\k)c=rng s by VALUED_0:21;
  dom(f^)/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
  then rng s c=left_open_halfline(x0) by A17,XBOOLE_1:1;
  then
A22: rng(s^\k)c=left_open_halfline(x0) by A21,XBOOLE_1:1;
A23: dom(f^)/\left_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
  then
A24: rng s c=dom(f^) by A17,XBOOLE_1:1;
  then
A25: rng s c=dom f by A20,XBOOLE_1:1;
  then
A26: rng(s^\k)c=dom f by A21,XBOOLE_1:1;
  then
A27: rng(s^\k)c=dom f/\left_open_halfline(x0) by A22,XBOOLE_1:19;
  then
A28: lim(f/*(s^\k))=0 by A1,A2,A15,A19,Def7;
  now
    let n;
A29: n in NAT by ORDINAL1:def 12;
    x0-r<s.(n+k) by A18,NAT_1:12;
    then
A30: x0-r<(s^\k).n by NAT_1:def 3;
A31: (s^\k).n in rng(s^\k) by VALUED_0:28;
    then (s^\k).n in left_open_halfline(x0) by A22;
    then (s^\k).n in {g1: g1<x0} by XXREAL_1:229;
    then ex g1 st g1=(s^\k).n & g1<x0;
    then (s^\k).n in {g2: x0-r<g2 & g2<x0} by A30;
    then (s^\k).n in ].x0-r,x0.[ by RCOMP_1:def 2;
    then (s^\k).n in dom f/\].x0-r,x0.[ by A26,A31,XBOOLE_0:def 4;
    then f.((s^\k).n)<0 by A4;
    hence (f/*(s^\k)).n<0 by A25,A21,FUNCT_2:108,XBOOLE_1:1,A29;
  end;
  then
A32: for n holds 0<=n implies (f/*(s^\k)).n<0;
  f/*(s^\k) is convergent by A1,A15,A19,A27;
  then
A33: (f/*(s^\k))" is divergent_to-infty by A28,A32,LIMFUNC1:36;
  (f/*(s^\k))"=((f/*s)^\k)" by A24,A20,VALUED_0:27,XBOOLE_1:1
    .=((f/*s)")^\k by SEQM_3:18
    .=((f^)/*s)^\k by A17,A23,RFUNCT_2:12,XBOOLE_1:1;
  hence thesis by A33,LIMFUNC1:7;
end;

theorem
  f is_right_convergent_in x0 & lim_right(f,x0)=0 & (ex r st 0<r & for g
  st g in dom f /\ ].x0,x0+r.[ holds 0<f.g) implies f^
  is_right_divergent_to+infty_in x0
proof
  assume that
A1: f is_right_convergent_in x0 and
A2: lim_right(f,x0)=0;
  given r such that
A3: 0<r and
A4: for g st g in dom f/\].x0,x0+r.[ holds 0<f.g;
  thus for r1 st x0<r1 ex g1 st g1<r1 & x0<g1 & g1 in dom(f^)
  proof
    let r1;
    assume x0<r1;
    then consider g1 such that
A5: g1<r1 and
A6: x0<g1 and
    g1 in dom f by A1;
    now
      per cases;
      suppose
A7:     g1<=x0+r;
        consider g2 such that
A8:     g2<g1 and
A9:     x0<g2 and
A10:    g2 in dom f by A1,A6;
        take g2;
        thus g2<r1 & x0<g2 by A5,A8,A9,XXREAL_0:2;
        g2<x0+r by A7,A8,XXREAL_0:2;
        then g2 in {r2: x0<r2 & r2<x0+r} by A9;
        then g2 in ].x0,x0+r.[ by RCOMP_1:def 2;
        then g2 in dom f/\].x0,x0+r.[ by A10,XBOOLE_0:def 4;
        then 0<>f.g2 by A4;
        then not f.g2 in {0} by TARSKI:def 1;
        then not g2 in f"{0} by FUNCT_1:def 7;
        then g2 in dom f\f"{0} by A10,XBOOLE_0:def 5;
        hence g2 in dom(f^) by RFUNCT_1:def 2;
      end;
      suppose
A11:    x0+r<=g1;
        x0<x0+r by A3,Lm1;
        then consider g2 such that
A12:    g2<x0+r and
A13:    x0<g2 and
A14:    g2 in dom f by A1;
        take g2;
        g2<g1 by A11,A12,XXREAL_0:2;
        hence g2<r1 & x0<g2 by A5,A13,XXREAL_0:2;
        g2 in {r2: x0<r2 & r2<x0+r} by A12,A13;
        then g2 in ].x0,x0+r.[ by RCOMP_1:def 2;
        then g2 in dom f/\].x0,x0+r.[ by A14,XBOOLE_0:def 4;
        then 0<>f.g2 by A4;
        then not f.g2 in {0} by TARSKI:def 1;
        then not g2 in f"{0} by FUNCT_1:def 7;
        then g2 in dom f\f"{0} by A14,XBOOLE_0:def 5;
        hence g2 in dom(f^) by RFUNCT_1:def 2;
      end;
    end;
    hence thesis;
  end;
  let s be Real_Sequence such that
A15: s is convergent and
A16: lim s=x0 and
A17: rng s c=dom(f^)/\right_open_halfline(x0);
  x0<x0+r by A3,Lm1;
  then consider k such that
A18: for n st k<=n holds s.n<x0+r by A15,A16,Th2;
A19: lim(s^\k)=x0 by A15,A16,SEQ_4:20;
  dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
  then
A20: dom(f^)c=dom f by XBOOLE_1:36;
A21: rng(s^\k)c=rng s by VALUED_0:21;
  dom(f^)/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
  then rng s c=right_open_halfline(x0) by A17,XBOOLE_1:1;
  then
A22: rng(s^\k)c=right_open_halfline(x0) by A21,XBOOLE_1:1;
A23: dom(f^)/\right_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
  then
A24: rng s c=dom(f^) by A17,XBOOLE_1:1;
  then
A25: rng s c=dom f by A20,XBOOLE_1:1;
  then
A26: rng(s^\k)c=dom f by A21,XBOOLE_1:1;
  then
A27: rng(s^\k)c=dom f/\right_open_halfline(x0) by A22,XBOOLE_1:19;
  then
A28: lim(f/*(s^\k))=0 by A1,A2,A15,A19,Def8;
  now
    let n;
A29: n in NAT by ORDINAL1:def 12;
    s.(n+k)<x0+r by A18,NAT_1:12;
    then
A30: (s^\k).n<x0+r by NAT_1:def 3;
A31: (s^\k).n in rng(s^\k) by VALUED_0:28;
    then (s^\k).n in right_open_halfline(x0) by A22;
    then (s^\k).n in {g1: x0<g1} by XXREAL_1:230;
    then ex g1 st g1=(s^\k).n & x0<g1;
    then (s^\k).n in {g2: x0<g2 & g2<x0+r} by A30;
    then (s^\k).n in ].x0,x0+r.[ by RCOMP_1:def 2;
    then (s^\k).n in dom f/\].x0,x0+r.[ by A26,A31,XBOOLE_0:def 4;
    then 0<f.((s^\k).n) by A4;
    hence 0<(f/*(s^\k)).n by A25,A21,FUNCT_2:108,XBOOLE_1:1,A29;
  end;
  then
A32: for n holds 0<=n implies 0<(f/*(s^\k)).n;
  f/*(s^\k) is convergent by A1,A15,A19,A27;
  then
A33: (f/*(s^\k))" is divergent_to+infty by A28,A32,LIMFUNC1:35;
  (f/*(s^\k))"=((f/*s)^\k)" by A24,A20,VALUED_0:27,XBOOLE_1:1
    .=((f/*s)")^\k by SEQM_3:18
    .=((f^)/*s)^\k by A17,A23,RFUNCT_2:12,XBOOLE_1:1;
  hence thesis by A33,LIMFUNC1:7;
end;

theorem
  f is_right_convergent_in x0 & lim_right(f,x0)=0 & (ex r st 0<r & for g
  st g in dom f /\ ].x0,x0+r.[ holds f.g<0) implies f^
  is_right_divergent_to-infty_in x0
proof
  assume that
A1: f is_right_convergent_in x0 and
A2: lim_right(f,x0)=0;
  given r such that
A3: 0<r and
A4: for g st g in dom f/\].x0,x0+r.[ holds f.g<0;
  thus for r1 st x0<r1 ex g1 st g1<r1 & x0<g1 & g1 in dom(f^)
  proof
    let r1;
    assume x0<r1;
    then consider g1 such that
A5: g1<r1 and
A6: x0<g1 and
    g1 in dom f by A1;
    now
      per cases;
      suppose
A7:     g1<=x0+r;
        consider g2 such that
A8:     g2<g1 and
A9:     x0<g2 and
A10:    g2 in dom f by A1,A6;
        take g2;
        thus g2<r1 & x0<g2 by A5,A8,A9,XXREAL_0:2;
        g2<x0+r by A7,A8,XXREAL_0:2;
        then g2 in {r2: x0<r2 & r2<x0+r} by A9;
        then g2 in ].x0,x0+r.[ by RCOMP_1:def 2;
        then g2 in dom f/\].x0,x0+r.[ by A10,XBOOLE_0:def 4;
        then not f.g2 in {0} by A4;
        then not g2 in f"{0} by FUNCT_1:def 7;
        then g2 in dom f\f"{0} by A10,XBOOLE_0:def 5;
        hence g2 in dom(f^) by RFUNCT_1:def 2;
      end;
      suppose
A11:    x0+r<=g1;
        x0<x0+r by A3,Lm1;
        then consider g2 such that
A12:    g2<x0+r and
A13:    x0<g2 and
A14:    g2 in dom f by A1;
        take g2;
        g2<g1 by A11,A12,XXREAL_0:2;
        hence g2<r1 & x0<g2 by A5,A13,XXREAL_0:2;
        g2 in {r2: x0<r2 & r2<x0+r} by A12,A13;
        then g2 in ].x0,x0+r.[ by RCOMP_1:def 2;
        then g2 in dom f/\].x0,x0+r.[ by A14,XBOOLE_0:def 4;
        then not f.g2 in {0} by A4;
        then not g2 in f"{0} by FUNCT_1:def 7;
        then g2 in dom f\f"{0} by A14,XBOOLE_0:def 5;
        hence g2 in dom(f^) by RFUNCT_1:def 2;
      end;
    end;
    hence thesis;
  end;
  let s be Real_Sequence such that
A15: s is convergent and
A16: lim s=x0 and
A17: rng s c=dom(f^)/\right_open_halfline(x0);
  x0<x0+r by A3,Lm1;
  then consider k such that
A18: for n st k<=n holds s.n<x0+r by A15,A16,Th2;
A19: lim(s^\k)=x0 by A15,A16,SEQ_4:20;
  dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
  then
A20: dom(f^)c=dom f by XBOOLE_1:36;
A21: rng(s^\k)c=rng s by VALUED_0:21;
  dom(f^)/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
  then rng s c=right_open_halfline(x0) by A17,XBOOLE_1:1;
  then
A22: rng(s^\k)c=right_open_halfline(x0) by A21,XBOOLE_1:1;
A23: dom(f^)/\right_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
  then
A24: rng s c=dom(f^) by A17,XBOOLE_1:1;
  then
A25: rng s c=dom f by A20,XBOOLE_1:1;
  then
A26: rng(s^\k)c=dom f by A21,XBOOLE_1:1;
  then
A27: rng(s^\k)c=dom f/\right_open_halfline(x0) by A22,XBOOLE_1:19;
  then
A28: lim(f/*(s^\k))=0 by A1,A2,A15,A19,Def8;
  now
    let n;
A29: n in NAT by ORDINAL1:def 12;
    s.(n+k)<x0+r by A18,NAT_1:12;
    then
A30: (s^\k).n<x0+r by NAT_1:def 3;
A31: (s^\k).n in rng(s^\k) by VALUED_0:28;
    then (s^\k).n in right_open_halfline(x0) by A22;
    then (s^\k).n in {g1: x0<g1} by XXREAL_1:230;
    then ex g1 st g1=(s^\k).n & x0<g1;
    then (s^\k).n in {g2: x0<g2 & g2<x0+r} by A30;
    then (s^\k).n in ].x0,x0+r.[ by RCOMP_1:def 2;
    then (s^\k).n in dom f/\].x0,x0+r.[ by A26,A31,XBOOLE_0:def 4;
    then f.((s^\k).n)<0 by A4;
    hence (f/*(s^\k)).n<0 by A25,A21,FUNCT_2:108,XBOOLE_1:1,A29;
  end;
  then
A32: for n holds 0<=n implies (f/*(s^\k)).n<0;
  f/*(s^\k) is convergent by A1,A15,A19,A27;
  then
A33: (f/*(s^\k))" is divergent_to-infty by A28,A32,LIMFUNC1:36;
  (f/*(s^\k))"=((f/*s)^\k)" by A24,A20,VALUED_0:27,XBOOLE_1:1
    .=((f/*s)")^\k by SEQM_3:18
    .=((f^)/*s)^\k by A17,A23,RFUNCT_2:12,XBOOLE_1:1;
  hence thesis by A33,LIMFUNC1:7;
end;

theorem
  f is_left_convergent_in x0 & lim_left(f,x0)=0 & (for r st r<x0 ex g st
r<g & g<x0 & g in dom f & f.g<>0) & (ex r st 0<r & for g st g in dom f /\ ].x0-
  r,x0.[ holds 0<=f.g) implies f^ is_left_divergent_to+infty_in x0
proof
  assume that
A1: f is_left_convergent_in x0 and
A2: lim_left(f,x0)=0 and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0;
  given r such that
A4: 0<r and
A5: for g st g in dom f/\].x0-r,x0.[ holds 0<=f.g;
  thus for r1 st r1<x0 ex g1 st r1<g1 & g1<x0 & g1 in dom(f^)
  proof
    let r1;
    assume r1<x0;
    then consider g1 such that
A6: r1<g1 and
A7: g1<x0 and
A8: g1 in dom f and
A9: f.g1<>0 by A3;
    take g1;
    thus r1<g1 & g1<x0 by A6,A7;
    not f.g1 in {0} by A9,TARSKI:def 1;
    then not g1 in f"{0} by FUNCT_1:def 7;
    then g1 in dom f\f"{0} by A8,XBOOLE_0:def 5;
    hence thesis by RFUNCT_1:def 2;
  end;
  let s be Real_Sequence such that
A10: s is convergent and
A11: lim s=x0 and
A12: rng s c=dom(f^)/\left_open_halfline(x0);
  x0-r<x0 by A4,Lm1;
  then consider k such that
A13: for n st k<=n holds x0-r<s.n by A10,A11,Th1;
A14: lim(s^\k)=x0 by A10,A11,SEQ_4:20;
A15: dom (f^)/\left_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
  then
A16: rng s c=dom(f^) by A12,XBOOLE_1:1;
A17: rng(s^\k)c=rng s by VALUED_0:21;
  dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
  then
A18: dom(f^)c=dom f by XBOOLE_1:36;
  then
A19: rng s c=dom f by A16,XBOOLE_1:1;
  then
A20: rng(s^\k)c=dom f by A17,XBOOLE_1:1;
  dom (f^)/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
  then rng s c=left_open_halfline(x0) by A12,XBOOLE_1:1;
  then
A21: rng(s^\k)c=left_open_halfline(x0) by A17,XBOOLE_1:1;
  then
A22: rng(s^\k)c=dom f/\left_open_halfline(x0) by A20,XBOOLE_1:19;
  then
A23: lim(f/*(s^\k))=0 by A1,A2,A10,A14,Def7;
A24: f/*(s^\k) is non-zero by A16,A17,RFUNCT_2:11,XBOOLE_1:1;
  now
    let n;
A25: n in NAT by ORDINAL1:def 12;
    x0-r<s.(n+k) by A13,NAT_1:12;
    then
A26: x0-r<(s^\k).n by NAT_1:def 3;
A27: (s^\k).n in rng(s^\k) by VALUED_0:28;
    then (s^\k).n in left_open_halfline(x0) by A21;
    then (s^\k).n in {g1: g1<x0} by XXREAL_1:229;
    then ex g1 st g1=(s^\k).n & g1<x0;
    then (s^\k).n in {g2: x0-r<g2 & g2<x0} by A26;
    then (s^\k).n in ].x0-r,x0.[ by RCOMP_1:def 2;
    then (s^\k).n in dom f/\].x0-r,x0.[ by A20,A27,XBOOLE_0:def 4;
    then
A28: 0<=f.((s^\k).n) by A5;
    (f/*(s^\k)).n<>0 by A24,SEQ_1:5;
    hence 0<(f/*(s^\k)).n by A19,A17,A28,FUNCT_2:108,XBOOLE_1:1,A25;
  end;
  then
A29: for n holds 0<=n implies 0<(f/*(s^\k)).n;
  f/*(s^\k) is convergent by A1,A10,A14,A22;
  then
A30: (f/*(s^\k))" is divergent_to+infty by A23,A29,LIMFUNC1:35;
  (f/*(s^\k))"=((f/*s)^\k)" by A16,A18,VALUED_0:27,XBOOLE_1:1
    .=((f/*s)")^\k by SEQM_3:18
    .=((f^)/*s)^\k by A12,A15,RFUNCT_2:12,XBOOLE_1:1;
  hence thesis by A30,LIMFUNC1:7;
end;

theorem
  f is_left_convergent_in x0 & lim_left(f,x0)=0 & (for r st r<x0 ex g st
r<g & g<x0 & g in dom f & f.g<>0) & (ex r st 0<r & for g st g in dom f /\ ].x0-
  r,x0.[ holds f.g<=0) implies f^ is_left_divergent_to-infty_in x0
proof
  assume that
A1: f is_left_convergent_in x0 and
A2: lim_left(f,x0)=0 and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0;
  given r such that
A4: 0<r and
A5: for g st g in dom f/\].x0-r,x0.[ holds f.g<=0;
  thus for r1 st r1<x0 ex g1 st r1<g1 & g1<x0 & g1 in dom(f^)
  proof
    let r1;
    assume r1<x0;
    then consider g1 such that
A6: r1<g1 and
A7: g1<x0 and
A8: g1 in dom f and
A9: f.g1<>0 by A3;
    take g1;
    thus r1<g1 & g1<x0 by A6,A7;
    not f.g1 in {0} by A9,TARSKI:def 1;
    then not g1 in f"{0} by FUNCT_1:def 7;
    then g1 in dom f\f"{0} by A8,XBOOLE_0:def 5;
    hence thesis by RFUNCT_1:def 2;
  end;
  let s be Real_Sequence such that
A10: s is convergent and
A11: lim s=x0 and
A12: rng s c=dom(f^)/\left_open_halfline(x0);
  x0-r<x0 by A4,Lm1;
  then consider k such that
A13: for n st k<=n holds x0-r<s.n by A10,A11,Th1;
A14: lim(s^\k)=x0 by A10,A11,SEQ_4:20;
A15: dom(f^)/\left_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
  then
A16: rng s c=dom(f^) by A12,XBOOLE_1:1;
A17: rng(s^\k)c=rng s by VALUED_0:21;
  dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
  then
A18: dom(f^)c=dom f by XBOOLE_1:36;
  then
A19: rng s c=dom f by A16,XBOOLE_1:1;
  then
A20: rng(s^\k)c=dom f by A17,XBOOLE_1:1;
  dom(f^)/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
  then rng s c=left_open_halfline(x0) by A12,XBOOLE_1:1;
  then
A21: rng(s^\k)c=left_open_halfline(x0) by A17,XBOOLE_1:1;
  then
A22: rng(s^\k)c=dom f/\left_open_halfline(x0) by A20,XBOOLE_1:19;
  then
A23: lim(f/*(s^\k))=0 by A1,A2,A10,A14,Def7;
A24: f/*(s^\k) is non-zero by A16,A17,RFUNCT_2:11,XBOOLE_1:1;
  now
    let n;
A25: n in NAT by ORDINAL1:def 12;
    x0-r<s.(n+k) by A13,NAT_1:12;
    then
A26: x0-r<(s^\k).n by NAT_1:def 3;
A27: (s^\k).n in rng(s^\k) by VALUED_0:28;
    then (s^\k).n in left_open_halfline(x0) by A21;
    then (s^\k).n in {g1: g1<x0} by XXREAL_1:229;
    then ex g1 st g1=(s^\k).n & g1<x0;
    then (s^\k).n in {g2: x0-r<g2 & g2<x0} by A26;
    then (s^\k).n in ].x0-r,x0.[ by RCOMP_1:def 2;
    then (s^\k).n in dom f/\].x0-r,x0.[ by A20,A27,XBOOLE_0:def 4;
    then
A28: f.((s^\k).n)<=0 by A5;
    (f/*(s^\k)).n<>0 by A24,SEQ_1:5;
    hence (f/*(s^\k)).n<0 by A19,A17,A28,FUNCT_2:108,XBOOLE_1:1,A25;
  end;
  then
A29: for n holds 0<=n implies (f/*(s^\k)).n<0;
  f/*(s^\k) is convergent by A1,A10,A14,A22;
  then
A30: (f/*(s^\k))" is divergent_to-infty by A23,A29,LIMFUNC1:36;
  (f/*(s^\k))"=((f/*s)^\k)" by A16,A18,VALUED_0:27,XBOOLE_1:1
    .=((f/*s)")^\k by SEQM_3:18
    .=((f^)/*s)^\k by A12,A15,RFUNCT_2:12,XBOOLE_1:1;
  hence thesis by A30,LIMFUNC1:7;
end;

theorem
  f is_right_convergent_in x0 & lim_right(f,x0)=0 & (for r st x0<r ex g
st g<r & x0<g & g in dom f & f.g<>0) & (ex r st 0<r & for g st g in dom f /\ ].
  x0,x0+r.[ holds 0<=f.g) implies f^ is_right_divergent_to+infty_in x0
proof
  assume that
A1: f is_right_convergent_in x0 and
A2: lim_right(f,x0)=0 and
A3: for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0;
  given r such that
A4: 0<r and
A5: for g st g in dom f/\].x0,x0+r.[ holds 0<=f.g;
  thus for r1 st x0<r1 ex g1 st g1<r1 & x0<g1 & g1 in dom(f^)
  proof
    let r1;
    assume x0<r1;
    then consider g1 such that
A6: g1<r1 and
A7: x0<g1 and
A8: g1 in dom f and
A9: f.g1<>0 by A3;
    take g1;
    thus g1<r1 & x0<g1 by A6,A7;
    not f.g1 in {0} by A9,TARSKI:def 1;
    then not g1 in f"{0} by FUNCT_1:def 7;
    then g1 in dom f\f"{0} by A8,XBOOLE_0:def 5;
    hence thesis by RFUNCT_1:def 2;
  end;
  let s be Real_Sequence such that
A10: s is convergent and
A11: lim s=x0 and
A12: rng s c=dom(f^)/\right_open_halfline(x0);
  x0<x0+r by A4,Lm1;
  then consider k such that
A13: for n st k<=n holds s.n<x0+r by A10,A11,Th2;
A14: lim(s^\k)=x0 by A10,A11,SEQ_4:20;
A15: dom(f^)/\right_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
  then
A16: rng s c=dom(f^) by A12,XBOOLE_1:1;
A17: rng(s^\k)c=rng s by VALUED_0:21;
  dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
  then
A18: dom(f^)c=dom f by XBOOLE_1:36;
  then
A19: rng s c=dom f by A16,XBOOLE_1:1;
  then
A20: rng(s^\k)c=dom f by A17,XBOOLE_1:1;
  dom(f^)/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
  then rng s c=right_open_halfline(x0) by A12,XBOOLE_1:1;
  then
A21: rng(s^\k)c=right_open_halfline(x0) by A17,XBOOLE_1:1;
  then
A22: rng(s^\k)c=dom f/\right_open_halfline(x0) by A20,XBOOLE_1:19;
  then
A23: lim(f/*(s^\k))=0 by A1,A2,A10,A14,Def8;
A24: f/*(s^\k) is non-zero by A16,A17,RFUNCT_2:11,XBOOLE_1:1;
  now
    let n;
A25: n in NAT by ORDINAL1:def 12;
    s.(n+k)<x0+r by A13,NAT_1:12;
    then
A26: (s^\k).n<x0+r by NAT_1:def 3;
A27: (s^\k).n in rng(s^\k) by VALUED_0:28;
    then (s^\k).n in right_open_halfline(x0) by A21;
    then (s^\k).n in {g1: x0<g1} by XXREAL_1:230;
    then ex g1 st g1=(s^\k).n & x0<g1;
    then (s^\k).n in {g2: x0<g2 & g2<x0+r} by A26;
    then (s^\k).n in ].x0,x0+r.[ by RCOMP_1:def 2;
    then (s^\k).n in dom f/\].x0,x0+r.[ by A20,A27,XBOOLE_0:def 4;
    then
A28: 0<=f.((s^\k).n) by A5;
    0<>(f/*(s^\k)).n by A24,SEQ_1:5;
    hence 0<(f/*(s^\k)).n by A19,A17,A28,FUNCT_2:108,XBOOLE_1:1,A25;
  end;
  then
A29: for n holds 0<=n implies 0<(f/*(s^\k)).n;
  f/*(s^\k) is convergent by A1,A10,A14,A22;
  then
A30: (f/*(s^\k))" is divergent_to+infty by A23,A29,LIMFUNC1:35;
  (f/*(s^\k))"=((f/*s)^\k)" by A16,A18,VALUED_0:27,XBOOLE_1:1
    .=((f/*s)")^\k by SEQM_3:18
    .=((f^)/*s)^\k by A12,A15,RFUNCT_2:12,XBOOLE_1:1;
  hence thesis by A30,LIMFUNC1:7;
end;

theorem
  f is_right_convergent_in x0 & lim_right(f,x0)=0 & (for r st x0<r ex g
st g<r & x0<g & g in dom f & f.g<>0) & (ex r st 0<r & for g st g in dom f /\ ].
  x0,x0+r.[ holds f.g<=0) implies f^ is_right_divergent_to-infty_in x0
proof
  assume that
A1: f is_right_convergent_in x0 and
A2: lim_right(f,x0)=0 and
A3: for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0;
  given r such that
A4: 0<r and
A5: for g st g in dom f/\].x0,x0+r.[ holds f.g<=0;
  thus for r1 st x0<r1 ex g1 st g1<r1 & x0<g1 & g1 in dom(f^)
  proof
    let r1;
    assume x0<r1;
    then consider g1 such that
A6: g1<r1 and
A7: x0<g1 and
A8: g1 in dom f and
A9: f.g1<>0 by A3;
    take g1;
    thus g1<r1 & x0<g1 by A6,A7;
    not f.g1 in {0} by A9,TARSKI:def 1;
    then not g1 in f"{0} by FUNCT_1:def 7;
    then g1 in dom f\f"{0} by A8,XBOOLE_0:def 5;
    hence thesis by RFUNCT_1:def 2;
  end;
  let s be Real_Sequence such that
A10: s is convergent and
A11: lim s=x0 and
A12: rng s c=dom(f^)/\right_open_halfline(x0);
  x0<x0+r by A4,Lm1;
  then consider k such that
A13: for n st k<=n holds s.n<x0+r by A10,A11,Th2;
A14: lim(s^\k)=x0 by A10,A11,SEQ_4:20;
A15: dom(f^)/\right_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
  then
A16: rng s c=dom(f^) by A12,XBOOLE_1:1;
A17: rng(s^\k)c=rng s by VALUED_0:21;
  dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
  then
A18: dom(f^)c=dom f by XBOOLE_1:36;
  then
A19: rng s c=dom f by A16,XBOOLE_1:1;
  then
A20: rng(s^\k)c=dom f by A17,XBOOLE_1:1;
  dom(f^)/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
  then rng s c=right_open_halfline(x0) by A12,XBOOLE_1:1;
  then
A21: rng(s^\k)c=right_open_halfline(x0) by A17,XBOOLE_1:1;
  then
A22: rng(s^\k)c=dom f/\right_open_halfline(x0) by A20,XBOOLE_1:19;
  then
A23: lim(f/*(s^\k))=0 by A1,A2,A10,A14,Def8;
A24: f/*(s^\k) is non-zero by A16,A17,RFUNCT_2:11,XBOOLE_1:1;
  now
    let n;
A25: n in NAT by ORDINAL1:def 12;
    s.(n+k)<x0+r by A13,NAT_1:12;
    then
A26: (s^\k).n<x0+r by NAT_1:def 3;
A27: (s^\k).n in rng(s^\k) by VALUED_0:28;
    then (s^\k).n in right_open_halfline(x0) by A21;
    then (s^\k).n in {g1: x0<g1} by XXREAL_1:230;
    then ex g1 st g1=(s^\k).n & x0<g1;
    then (s^\k).n in {g2: x0<g2 & g2<x0+r} by A26;
    then (s^\k).n in ].x0,x0+r.[ by RCOMP_1:def 2;
    then (s^\k).n in dom f/\].x0,x0+r.[ by A20,A27,XBOOLE_0:def 4;
    then
A28: f.((s^\k).n)<=0 by A5;
    (f/*(s^\k)).n<>0 by A24,SEQ_1:5;
    hence (f/*(s^\k)).n<0 by A19,A17,A28,FUNCT_2:108,XBOOLE_1:1,A25;
  end;
  then
A29: for n holds 0<=n implies (f/*(s^\k)).n<0;
  f/*(s^\k) is convergent by A1,A10,A14,A22;
  then
A30: (f/*(s^\k))" is divergent_to-infty by A23,A29,LIMFUNC1:36;
  (f/*(s^\k))"=((f/*s)^\k)" by A16,A18,VALUED_0:27,XBOOLE_1:1
    .=((f/*s)")^\k by SEQM_3:18
    .=((f^)/*s)^\k by A12,A15,RFUNCT_2:12,XBOOLE_1:1;
  hence thesis by A30,LIMFUNC1:7;
end;