:: The Limit of a Composition of Real Functions
::  by Jaros{\l}aw Kotowicz
::
:: Received September 5, 1990
:: Copyright (c) 1990-2016 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 REAL_1, PARTFUN1, NUMBERS, CARD_1, ARYTM_3, ARYTM_1, SEQ_1,
      RELAT_1, TARSKI, FUNCT_2, SUBSET_1, FUNCT_1, XBOOLE_0, LIMFUNC1,
      LIMFUNC2, SEQ_2, ORDINAL2, XXREAL_1, XXREAL_0, NAT_1, LIMFUNC3;
 notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, SEQ_1, SEQ_2, VALUED_0, RCOMP_1, RELSET_1, FUNCT_1,
      PARTFUN1, FUNCT_2, LIMFUNC1, LIMFUNC2, LIMFUNC3;
 constructors PARTFUN1, REAL_1, NAT_1, SEQ_2, SEQM_3, PROB_1, RCOMP_1,
      RFUNCT_2, LIMFUNC1, LIMFUNC2, LIMFUNC3, MEMBERED, RELSET_1, COMSEQ_2;
 registrations RELSET_1, VALUED_0, ORDINAL1, NUMBERS, XBOOLE_0, SEQ_4, FUNCT_2,
      XREAL_0, NAT_1;
 requirements SUBSET, ARITHM, BOOLE, NUMERALS;
 definitions TARSKI;
 equalities PROB_1, LIMFUNC1;
 expansions TARSKI, LIMFUNC1;
 theorems TARSKI, NAT_1, FUNCT_1, SEQ_4, RCOMP_1, LIMFUNC1, LIMFUNC2, LIMFUNC3,
      RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_1, FUNCT_2, VALUED_0,
      ORDINAL1;

begin

reserve r,r1,r2,g,g1,g2,x0 for Real;
reserve f1,f2 for PartFunc of REAL,REAL;

Lm1: 0 < g implies r-g<r & r<r+g
proof
  assume
A1: 0<g;
  then r-g<r-0 by XREAL_1:15;
  hence r-g<r;
  r+0<r+g by A1,XREAL_1:8;
  hence thesis;
end;

Lm2: for s be Real_Sequence st rng s c=dom(f2*f1) holds rng s c=dom f1 & rng(
f1/*s)c=dom f2
proof
  let s be Real_Sequence such that
A1: rng s c=dom(f2*f1);
A2: dom(f2*f1)c=dom f1 by RELAT_1:25;
  hence rng s c=dom f1 by A1;
  let x be object;
  assume x in rng(f1/*s);
  then consider n be Element of NAT such that
A3: (f1/*s).n=x by FUNCT_2:113;
  s.n in rng s by VALUED_0:28;
  then f1.(s.n) in dom f2 by A1,FUNCT_1:11;
  hence thesis by A1,A2,A3,FUNCT_2:108,XBOOLE_1:1;
end;

theorem Th1:
  for s be Real_Sequence,X be set st rng s c= dom(f2*f1) /\ X holds
rng s c= dom(f2*f1) & rng s c= X & rng s c= dom f1 & rng s c= dom f1 /\ X & rng
  (f1/*s) c= dom f2
proof
  let s be Real_Sequence,X be set;
  assume rng s c=dom(f2*f1)/\X;
  hence
A1: rng s c=dom(f2*f1) & rng s c=X by XBOOLE_1:18;
A2: dom(f2*f1)c=dom f1 by RELAT_1:25;
  hence rng s c=dom f1 by A1;
  hence rng s c=dom f1/\X by A1,XBOOLE_1:19;
  let x be object;
  assume x in rng(f1/*s);
  then consider n be Element of NAT such that
A3: (f1/*s).n=x by FUNCT_2:113;
  s.n in rng s by VALUED_0:28;
  then f1.(s.n) in dom f2 by A1,FUNCT_1:11;
  hence thesis by A1,A2,A3,FUNCT_2:108,XBOOLE_1:1;
end;

theorem Th2:
  for s be Real_Sequence,X be set st rng s c= dom(f2*f1) \ X holds
rng s c= dom(f2*f1) & rng s c= dom f1 & rng s c= dom f1 \ X & rng(f1/*s) c= dom
  f2
proof
  let s be Real_Sequence,X be set such that
A1: rng s c=dom(f2*f1)\X;
  dom(f2*f1)\X c=dom(f2*f1) by XBOOLE_1:36;
  hence
A2: rng s c=dom(f2*f1) by A1;
A3: dom(f2*f1)c=dom f1 by RELAT_1:25;
  hence
A4: rng s c=dom f1 by A2;
  thus rng s c=dom f1\X
  proof
    let x be object;
    assume
A5: x in rng s;
    then not x in X by A1,XBOOLE_0:def 5;
    hence thesis by A4,A5,XBOOLE_0:def 5;
  end;
  let x be object;
  assume x in rng(f1/*s);
  then consider n be Element of NAT such that
A6: (f1/*s).n=x by FUNCT_2:113;
  s.n in rng s by VALUED_0:28;
  then f1.(s.n) in dom f2 by A2,FUNCT_1:11;
  hence thesis by A2,A3,A6,FUNCT_2:108,XBOOLE_1:1;
end;

theorem
  f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to+infty
  & (for r ex g st r<g & g in dom(f2*f1)) implies f2*f1 is
  divergent_in+infty_to+infty
proof
  assume that
A1: f1 is divergent_in+infty_to+infty and
A2: f2 is divergent_in+infty_to+infty and
A3: for r ex g st r<g & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is divergent_to+infty and
A5: rng s c=dom(f2*f1);
    rng s c=dom f1 by A5,Lm2;
    then
A6: f1/*s is divergent_to+infty by A1,A4;
    rng(f1/*s)c=dom f2 by A5,Lm2;
    then f2/*(f1/*s) is divergent_to+infty by A2,A6;
    hence (f2*f1)/*s is divergent_to+infty by A5,VALUED_0:31;
  end;
  hence thesis by A3;
end;

theorem
  f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to-infty
  & (for r ex g st r<g & g in dom(f2*f1)) implies f2*f1 is
  divergent_in+infty_to-infty
proof
  assume that
A1: f1 is divergent_in+infty_to+infty and
A2: f2 is divergent_in+infty_to-infty and
A3: for r ex g st r<g & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is divergent_to+infty and
A5: rng s c=dom(f2*f1);
    rng s c=dom f1 by A5,Lm2;
    then
A6: f1/*s is divergent_to+infty by A1,A4;
    rng(f1/*s)c=dom f2 by A5,Lm2;
    then f2/*(f1/*s) is divergent_to-infty by A2,A6;
    hence (f2*f1)/*s is divergent_to-infty by A5,VALUED_0:31;
  end;
  hence thesis by A3;
end;

theorem
  f1 is divergent_in+infty_to-infty & f2 is divergent_in-infty_to+infty
  & (for r ex g st r<g & g in dom(f2*f1)) implies f2*f1 is
  divergent_in+infty_to+infty
proof
  assume that
A1: f1 is divergent_in+infty_to-infty and
A2: f2 is divergent_in-infty_to+infty and
A3: for r ex g st r<g & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is divergent_to+infty and
A5: rng s c=dom(f2*f1);
    rng s c=dom f1 by A5,Lm2;
    then
A6: f1/*s is divergent_to-infty by A1,A4;
    rng(f1/*s)c=dom f2 by A5,Lm2;
    then f2/*(f1/*s) is divergent_to+infty by A2,A6;
    hence (f2*f1)/*s is divergent_to+infty by A5,VALUED_0:31;
  end;
  hence thesis by A3;
end;

theorem
  f1 is divergent_in+infty_to-infty & f2 is divergent_in-infty_to-infty
  & (for r ex g st r<g & g in dom(f2*f1)) implies f2*f1 is
  divergent_in+infty_to-infty
proof
  assume that
A1: f1 is divergent_in+infty_to-infty and
A2: f2 is divergent_in-infty_to-infty and
A3: for r ex g st r<g & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is divergent_to+infty and
A5: rng s c=dom(f2*f1);
    rng s c=dom f1 by A5,Lm2;
    then
A6: f1/*s is divergent_to-infty by A1,A4;
    rng(f1/*s)c=dom f2 by A5,Lm2;
    then f2/*(f1/*s) is divergent_to-infty by A2,A6;
    hence (f2*f1)/*s is divergent_to-infty by A5,VALUED_0:31;
  end;
  hence thesis by A3;
end;

theorem
  f1 is divergent_in-infty_to+infty & f2 is divergent_in+infty_to+infty
  & (for r ex g st g<r & g in dom(f2*f1)) implies f2*f1 is
  divergent_in-infty_to+infty
proof
  assume that
A1: f1 is divergent_in-infty_to+infty and
A2: f2 is divergent_in+infty_to+infty and
A3: for r ex g st g<r & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is divergent_to-infty and
A5: rng s c=dom(f2*f1);
    rng s c=dom f1 by A5,Lm2;
    then
A6: f1/*s is divergent_to+infty by A1,A4;
    rng(f1/*s)c=dom f2 by A5,Lm2;
    then f2/*(f1/*s) is divergent_to+infty by A2,A6;
    hence (f2*f1)/*s is divergent_to+infty by A5,VALUED_0:31;
  end;
  hence thesis by A3;
end;

theorem
  f1 is divergent_in-infty_to+infty & f2 is divergent_in+infty_to-infty
  & (for r ex g st g<r & g in dom(f2*f1)) implies f2*f1 is
  divergent_in-infty_to-infty
proof
  assume that
A1: f1 is divergent_in-infty_to+infty and
A2: f2 is divergent_in+infty_to-infty and
A3: for r ex g st g<r & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is divergent_to-infty and
A5: rng s c=dom(f2*f1);
    rng s c=dom f1 by A5,Lm2;
    then
A6: f1/*s is divergent_to+infty by A1,A4;
    rng(f1/*s)c=dom f2 by A5,Lm2;
    then f2/*(f1/*s) is divergent_to-infty by A2,A6;
    hence (f2*f1)/*s is divergent_to-infty by A5,VALUED_0:31;
  end;
  hence thesis by A3;
end;

theorem
  f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to+infty
  & (for r ex g st g<r & g in dom(f2*f1)) implies f2*f1 is
  divergent_in-infty_to+infty
proof
  assume that
A1: f1 is divergent_in-infty_to-infty and
A2: f2 is divergent_in-infty_to+infty and
A3: for r ex g st g<r & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is divergent_to-infty and
A5: rng s c=dom(f2*f1);
    rng s c=dom f1 by A5,Lm2;
    then
A6: f1/*s is divergent_to-infty by A1,A4;
    rng(f1/*s)c=dom f2 by A5,Lm2;
    then f2/*(f1/*s) is divergent_to+infty by A2,A6;
    hence (f2*f1)/*s is divergent_to+infty by A5,VALUED_0:31;
  end;
  hence thesis by A3;
end;

theorem
  f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to-infty
  & (for r ex g st g<r & g in dom(f2*f1)) implies f2*f1 is
  divergent_in-infty_to-infty
proof
  assume that
A1: f1 is divergent_in-infty_to-infty and
A2: f2 is divergent_in-infty_to-infty and
A3: for r ex g st g<r & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is divergent_to-infty and
A5: rng s c=dom(f2*f1);
    rng s c=dom f1 by A5,Lm2;
    then
A6: f1/*s is divergent_to-infty by A1,A4;
    rng(f1/*s)c=dom f2 by A5,Lm2;
    then f2/*(f1/*s) is divergent_to-infty by A2,A6;
    hence (f2*f1)/*s is divergent_to-infty by A5,VALUED_0:31;
  end;
  hence thesis by A3;
end;

theorem
  f1 is_left_divergent_to+infty_in x0 & f2 is
divergent_in+infty_to+infty & (for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*
  f1)) implies f2*f1 is_left_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_left_divergent_to+infty_in x0 and
A2: f2 is divergent_in+infty_to+infty and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is convergent & lim s=x0 and
A5: rng s c=dom(f2*f1)/\left_open_halfline(x0);
A6: rng s c=dom(f2*f1) by A5,Th1;
    rng s c=dom f1/\left_open_halfline(x0) by A5,Th1;
    then
A7: f1/*s is divergent_to+infty by A1,A4,LIMFUNC2:def 2;
    rng(f1/*s)c=dom f2 by A5,Th1;
    then f2/*(f1/*s) is divergent_to+infty by A2,A7;
    hence (f2*f1)/*s is divergent_to+infty by A6,VALUED_0:31;
  end;
  hence thesis by A3,LIMFUNC2:def 2;
end;

theorem
  f1 is_left_divergent_to+infty_in x0 & f2 is
divergent_in+infty_to-infty & (for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*
  f1)) implies f2*f1 is_left_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_left_divergent_to+infty_in x0 and
A2: f2 is divergent_in+infty_to-infty and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is convergent & lim s=x0 and
A5: rng s c=dom(f2*f1)/\left_open_halfline(x0);
A6: rng s c=dom(f2*f1) by A5,Th1;
    rng s c=dom f1/\left_open_halfline(x0) by A5,Th1;
    then
A7: f1/*s is divergent_to+infty by A1,A4,LIMFUNC2:def 2;
    rng(f1/*s)c=dom f2 by A5,Th1;
    then f2/*(f1/*s) is divergent_to-infty by A2,A7;
    hence (f2*f1)/*s is divergent_to-infty by A6,VALUED_0:31;
  end;
  hence thesis by A3,LIMFUNC2:def 3;
end;

theorem
  f1 is_left_divergent_to-infty_in x0 & f2 is
divergent_in-infty_to+infty & (for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*
  f1)) implies f2*f1 is_left_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_left_divergent_to-infty_in x0 and
A2: f2 is divergent_in-infty_to+infty and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is convergent & lim s=x0 and
A5: rng s c=dom(f2*f1)/\left_open_halfline(x0);
A6: rng s c=dom(f2*f1) by A5,Th1;
    rng s c=dom f1/\left_open_halfline(x0) by A5,Th1;
    then
A7: f1/*s is divergent_to-infty by A1,A4,LIMFUNC2:def 3;
    rng(f1/*s)c=dom f2 by A5,Th1;
    then f2/*(f1/*s) is divergent_to+infty by A2,A7;
    hence (f2*f1)/*s is divergent_to+infty by A6,VALUED_0:31;
  end;
  hence thesis by A3,LIMFUNC2:def 2;
end;

theorem
  f1 is_left_divergent_to-infty_in x0 & f2 is
divergent_in-infty_to-infty & (for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*
  f1)) implies f2*f1 is_left_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_left_divergent_to-infty_in x0 and
A2: f2 is divergent_in-infty_to-infty and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is convergent & lim s=x0 and
A5: rng s c=dom(f2*f1)/\left_open_halfline(x0);
A6: rng s c=dom(f2*f1) by A5,Th1;
    rng s c=dom f1/\left_open_halfline(x0) by A5,Th1;
    then
A7: f1/*s is divergent_to-infty by A1,A4,LIMFUNC2:def 3;
    rng(f1/*s)c=dom f2 by A5,Th1;
    then f2/*(f1/*s) is divergent_to-infty by A2,A7;
    hence (f2*f1)/*s is divergent_to-infty by A6,VALUED_0:31;
  end;
  hence thesis by A3,LIMFUNC2:def 3;
end;

theorem
  f1 is_right_divergent_to+infty_in x0 & f2 is
divergent_in+infty_to+infty & (for r st x0<r ex g st g<r & x0<g & g in dom(f2*
  f1)) implies f2*f1 is_right_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_right_divergent_to+infty_in x0 and
A2: f2 is divergent_in+infty_to+infty and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is convergent & lim s=x0 and
A5: rng s c=dom(f2*f1)/\right_open_halfline(x0);
A6: rng s c=dom(f2*f1) by A5,Th1;
    rng s c=dom f1/\right_open_halfline(x0) by A5,Th1;
    then
A7: f1/*s is divergent_to+infty by A1,A4,LIMFUNC2:def 5;
    rng(f1/*s)c=dom f2 by A5,Th1;
    then f2/*(f1/*s) is divergent_to+infty by A2,A7;
    hence (f2*f1)/*s is divergent_to+infty by A6,VALUED_0:31;
  end;
  hence thesis by A3,LIMFUNC2:def 5;
end;

theorem
  f1 is_right_divergent_to+infty_in x0 & f2 is
divergent_in+infty_to-infty & (for r st x0<r ex g st g<r & x0<g & g in dom(f2*
  f1)) implies f2*f1 is_right_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_right_divergent_to+infty_in x0 and
A2: f2 is divergent_in+infty_to-infty and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is convergent & lim s=x0 and
A5: rng s c=dom(f2*f1)/\right_open_halfline(x0);
A6: rng s c=dom(f2*f1) by A5,Th1;
    rng s c=dom f1/\right_open_halfline(x0) by A5,Th1;
    then
A7: f1/*s is divergent_to+infty by A1,A4,LIMFUNC2:def 5;
    rng(f1/*s)c=dom f2 by A5,Th1;
    then f2/*(f1/*s) is divergent_to-infty by A2,A7;
    hence (f2*f1)/*s is divergent_to-infty by A6,VALUED_0:31;
  end;
  hence thesis by A3,LIMFUNC2:def 6;
end;

theorem
  f1 is_right_divergent_to-infty_in x0 & f2 is
divergent_in-infty_to+infty & (for r st x0<r ex g st g<r & x0<g & g in dom(f2*
  f1)) implies f2*f1 is_right_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_right_divergent_to-infty_in x0 and
A2: f2 is divergent_in-infty_to+infty and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is convergent & lim s=x0 and
A5: rng s c=dom(f2*f1)/\right_open_halfline(x0);
A6: rng s c=dom(f2*f1) by A5,Th1;
    rng s c=dom f1/\right_open_halfline(x0) by A5,Th1;
    then
A7: f1/*s is divergent_to-infty by A1,A4,LIMFUNC2:def 6;
    rng(f1/*s)c=dom f2 by A5,Th1;
    then f2/*(f1/*s) is divergent_to+infty by A2,A7;
    hence (f2*f1)/*s is divergent_to+infty by A6,VALUED_0:31;
  end;
  hence thesis by A3,LIMFUNC2:def 5;
end;

theorem
  f1 is_right_divergent_to-infty_in x0 & f2 is
divergent_in-infty_to-infty & (for r st x0<r ex g st g<r & x0<g & g in dom(f2*
  f1)) implies f2*f1 is_right_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_right_divergent_to-infty_in x0 and
A2: f2 is divergent_in-infty_to-infty and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is convergent & lim s=x0 and
A5: rng s c=dom(f2*f1)/\right_open_halfline(x0);
A6: rng s c=dom(f2*f1) by A5,Th1;
    rng s c=dom f1/\right_open_halfline(x0) by A5,Th1;
    then
A7: f1/*s is divergent_to-infty by A1,A4,LIMFUNC2:def 6;
    rng(f1/*s)c=dom f2 by A5,Th1;
    then f2/*(f1/*s) is divergent_to-infty by A2,A7;
    hence (f2*f1)/*s is divergent_to-infty by A6,VALUED_0:31;
  end;
  hence thesis by A3,LIMFUNC2:def 6;
end;

theorem
  f1 is_left_convergent_in x0 & f2 is_left_divergent_to+infty_in
lim_left(f1,x0) & (for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1)) & (ex g
  st 0<g & for r st r in dom f1 /\ ].x0-g,x0.[ holds f1.r<lim_left(f1,x0))
  implies f2*f1 is_left_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_left_divergent_to+infty_in lim_left(f1,x0) and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0-g,x0.[ holds f1.r<lim_left(f1,x0);
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)/\left_open_halfline(x0);
    consider k be Nat such that
A8: for n be Nat st k<=n holds x0-g<s.n by A4,A6,Lm1,LIMFUNC2:1;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th1;
    rng(f1/*s)c=dom f2 by A7,Th1;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1/\left_open_halfline(x0) by A7,Th1;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC2:def 7;
A13: rng s c=dom f1 by A7,Th1;
A14: rng s c=left_open_halfline(x0) by A7,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A15:  q.n=x by FUNCT_2:113;
A16:   n+k in NAT by ORDINAL1:def 12;
A17:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108,A16
        .=x by A15,NAT_1:def 3;
A18:  x0-g<s.(n+k) by A8,NAT_1:12;
A19:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in left_open_halfline(x0) by A14;
      then s.(n+k) in {g1 : g1<x0} by XXREAL_1:229;
      then ex g1 st g1=s.(n+k) & g1<x0;
      then s.(n+k) in {g2: x0-g<g2 & g2<x0} by A18;
      then s.(n+k) in ].x0-g,x0.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0-g,x0.[ by A13,A19,XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim_left(f1,x0) by A5;
      then f1.(s.(n+k)) in {r1 : r1<lim_left(f1,x0)};
      then
A20:  f1.(s.(n+k)) in left_open_halfline(lim_left(f1,x0)) by XXREAL_1:229;
      f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11;
      hence x in dom f2/\left_open_halfline(lim_left(f1,x0)) by A20,A17,
XBOOLE_0:def 4;
    end;
    then
A21: rng q c=dom f2/\left_open_halfline(lim_left(f1,x0));
    lim(f1/*s)=lim_left(f1,x0) by A1,A6,A11,LIMFUNC2:def 7;
    then lim q=lim_left(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to+infty by A2,A12,A21,LIMFUNC2:def 2;
    hence (f2*f1)/*s is divergent_to+infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC2:def 2;
end;

theorem
  f1 is_left_convergent_in x0 & f2 is_left_divergent_to-infty_in
lim_left(f1,x0) & (for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1)) & (ex g
  st 0<g & for r st r in dom f1 /\ ].x0-g,x0.[ holds f1.r<lim_left(f1,x0))
  implies f2*f1 is_left_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_left_divergent_to-infty_in lim_left(f1,x0) and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0-g,x0.[ holds f1.r<lim_left(f1,x0);
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)/\left_open_halfline(x0);
    consider k be Nat such that
A8: for n be Nat st k<=n holds x0-g<s.n by A4,A6,Lm1,LIMFUNC2:1;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th1;
    rng(f1/*s)c=dom f2 by A7,Th1;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1/\left_open_halfline(x0) by A7,Th1;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC2:def 7;
A13: rng s c=dom f1 by A7,Th1;
A14: rng s c=left_open_halfline(x0) by A7,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A15:  q.n=x by FUNCT_2:113;
A16:   n+k in NAT by ORDINAL1:def 12;
A17:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108,A16
        .=x by A15,NAT_1:def 3;
A18:  x0-g<s.(n+k) by A8,NAT_1:12;
A19:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in left_open_halfline(x0) by A14;
      then s.(n+k) in {g1: g1<x0} by XXREAL_1:229;
      then ex g1 st g1=s.(n+k) & g1<x0;
      then s.(n+k) in {g2 : x0-g<g2 & g2<x0} by A18;
      then s.(n+k) in ].x0-g,x0.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0-g,x0.[ by A13,A19,XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim_left(f1,x0) by A5;
      then f1.(s.(n+k)) in {r1: r1<lim_left(f1,x0)};
      then
A20:  f1.(s.(n+k)) in left_open_halfline(lim_left(f1,x0)) by XXREAL_1:229;
      f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11;
      hence x in dom f2/\left_open_halfline(lim_left(f1,x0)) by A20,A17,
XBOOLE_0:def 4;
    end;
    then
A21: rng q c=dom f2/\left_open_halfline(lim_left(f1,x0));
    lim(f1/*s)=lim_left(f1,x0) by A1,A6,A11,LIMFUNC2:def 7;
    then lim q=lim_left(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to-infty by A2,A12,A21,LIMFUNC2:def 3;
    hence (f2*f1)/*s is divergent_to-infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC2:def 3;
end;

theorem
  f1 is_left_convergent_in x0 & f2 is_right_divergent_to+infty_in
lim_left(f1,x0) & (for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1)) & (ex g
  st 0<g & for r st r in dom f1 /\ ].x0-g,x0.[ holds lim_left(f1,x0)<f1.r)
  implies f2*f1 is_left_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_right_divergent_to+infty_in lim_left(f1,x0) and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0-g,x0.[ holds lim_left(f1,x0)<f1.r;
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)/\left_open_halfline(x0);
    consider k be Nat such that
A8: for n be Nat st k<=n holds x0-g<s.n by A4,A6,Lm1,LIMFUNC2:1;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th1;
    rng(f1/*s)c=dom f2 by A7,Th1;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1/\left_open_halfline(x0) by A7,Th1;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC2:def 7;
A13: rng s c=dom f1 by A7,Th1;
A14: rng s c=left_open_halfline(x0) by A7,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A15:  q.n=x by FUNCT_2:113;
A16:   n+k in NAT by ORDINAL1:def 12;
A17:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108,A16
        .=x by A15,NAT_1:def 3;
A18:  x0-g<s.(n+k) by A8,NAT_1:12;
A19:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in left_open_halfline(x0) by A14;
      then s.(n+k) in {g1: g1<x0} by XXREAL_1:229;
      then ex g1 st g1=s.(n+k) & g1<x0;
      then s.(n+k) in {g2: x0-g<g2 & g2<x0} by A18;
      then s.(n+k) in ].x0-g,x0.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0-g,x0.[ by A13,A19,XBOOLE_0:def 4;
      then lim_left(f1,x0)<f1.(s.(n+k)) by A5;
      then f1.(s.(n+k)) in {r1: lim_left(f1,x0)<r1};
      then
A20:  f1.(s.(n+k)) in right_open_halfline(lim_left(f1,x0)) by XXREAL_1:230;
      f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11;
      hence x in dom f2/\right_open_halfline(lim_left(f1,x0)) by A20,A17,
XBOOLE_0:def 4;
    end;
    then
A21: rng q c=dom f2/\right_open_halfline(lim_left(f1,x0));
    lim(f1/*s)=lim_left(f1,x0) by A1,A6,A11,LIMFUNC2:def 7;
    then lim q=lim_left(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to+infty by A2,A12,A21,LIMFUNC2:def 5;
    hence (f2*f1)/*s is divergent_to+infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC2:def 2;
end;

theorem
  f1 is_left_convergent_in x0 & f2 is_right_divergent_to-infty_in
lim_left(f1,x0) & (for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1)) & (ex g
  st 0<g & for r st r in dom f1 /\ ].x0-g,x0.[ holds lim_left(f1,x0)<f1.r)
  implies f2*f1 is_left_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_right_divergent_to-infty_in lim_left(f1,x0) and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0-g,x0.[ holds lim_left(f1,x0)<f1.r;
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)/\left_open_halfline(x0);
    consider k be Nat such that
A8: for n be Nat st k<=n holds x0-g<s.n by A4,A6,Lm1,LIMFUNC2:1;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th1;
    rng(f1/*s)c=dom f2 by A7,Th1;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1/\left_open_halfline(x0) by A7,Th1;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC2:def 7;
A13: rng s c=dom f1 by A7,Th1;
A14: rng s c=left_open_halfline(x0) by A7,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A15:  q.n=x by FUNCT_2:113;
A16:   n+k in NAT by ORDINAL1:def 12;
A17:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108,A16
        .=x by A15,NAT_1:def 3;
A18:  x0-g<s.(n+k) by A8,NAT_1:12;
A19:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in left_open_halfline(x0) by A14;
      then s.(n+k) in {g1: g1<x0} by XXREAL_1:229;
      then ex g1 st g1=s.(n+k) & g1<x0;
      then s.(n+k) in {g2: x0-g<g2 & g2<x0} by A18;
      then s.(n+k) in ].x0-g,x0.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0-g,x0.[ by A13,A19,XBOOLE_0:def 4;
      then lim_left(f1,x0)<f1.(s.(n+k)) by A5;
      then f1.(s.(n+k)) in {r1: lim_left(f1,x0)<r1};
      then
A20:  f1.(s.(n+k)) in right_open_halfline(lim_left(f1,x0)) by XXREAL_1:230;
      f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11;
      hence x in dom f2/\right_open_halfline(lim_left(f1,x0)) by A20,A17,
XBOOLE_0:def 4;
    end;
    then
A21: rng q c=dom f2/\right_open_halfline(lim_left(f1,x0));
    lim(f1/*s)=lim_left(f1,x0) by A1,A6,A11,LIMFUNC2:def 7;
    then lim q=lim_left(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to-infty by A2,A12,A21,LIMFUNC2:def 6;
    hence (f2*f1)/*s is divergent_to-infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC2:def 3;
end;

theorem
  f1 is_right_convergent_in x0 & f2 is_right_divergent_to+infty_in
lim_right(f1,x0) & (for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1)) & (ex g
  st 0<g & for r st r in dom f1 /\ ].x0,x0+g.[ holds lim_right(f1,x0)<f1.r)
  implies f2*f1 is_right_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_right_divergent_to+infty_in lim_right(f1,x0) and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0,x0+g.[ holds lim_right(f1,x0)<f1.r;
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)/\right_open_halfline(x0);
    consider k be Nat such that
A8: for n be Nat st k<=n holds s.n<x0+g by A4,A6,Lm1,LIMFUNC2:2;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th1;
    rng(f1/*s)c=dom f2 by A7,Th1;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1/\right_open_halfline(x0) by A7,Th1;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC2:def 8;
A13: rng s c=dom f1 by A7,Th1;
A14: rng s c=right_open_halfline(x0) by A7,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A15:  q.n=x by FUNCT_2:113;
A16:   n+k in NAT by ORDINAL1:def 12;
A17:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108,A16
        .=x by A15,NAT_1:def 3;
A18:  s.(n+k)<x0+g by A8,NAT_1:12;
A19:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in right_open_halfline(x0) by A14;
      then s.(n+k) in {g1: x0<g1} by XXREAL_1:230;
      then ex g1 st g1=s.(n+k) & x0<g1;
      then s.(n+k) in {g2: x0<g2 & g2<x0+g} by A18;
      then s.(n+k) in ].x0,x0+g.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0,x0+g.[ by A13,A19,XBOOLE_0:def 4;
      then lim_right(f1,x0)<f1.(s.(n+k)) by A5;
      then f1.(s.(n+k)) in {r1: lim_right(f1,x0)<r1};
      then
A20:  f1.(s.(n+k)) in right_open_halfline(lim_right(f1,x0)) by XXREAL_1:230;
      f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11;
      hence x in dom f2/\right_open_halfline(lim_right(f1,x0)) by A20,A17,
XBOOLE_0:def 4;
    end;
    then
A21: rng q c=dom f2/\ right_open_halfline(lim_right(f1,x0));
    lim(f1/*s)=lim_right(f1,x0) by A1,A6,A11,LIMFUNC2:def 8;
    then lim q=lim_right(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to+infty by A2,A12,A21,LIMFUNC2:def 5;
    hence (f2*f1)/*s is divergent_to+infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC2:def 5;
end;

theorem
  f1 is_right_convergent_in x0 & f2 is_right_divergent_to-infty_in
lim_right(f1,x0) & (for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1)) & (ex g
  st 0<g & for r st r in dom f1 /\ ].x0,x0+g.[ holds lim_right(f1,x0)<f1.r)
  implies f2*f1 is_right_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_right_divergent_to-infty_in lim_right(f1,x0) and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0,x0+g.[ holds lim_right(f1,x0)<f1.r;
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)/\right_open_halfline(x0);
    consider k be Nat such that
A8: for n be Nat st k<=n holds s.n<x0+g by A4,A6,Lm1,LIMFUNC2:2;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th1;
    rng(f1/*s)c=dom f2 by A7,Th1;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1/\right_open_halfline(x0) by A7,Th1;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC2:def 8;
A13: rng s c=dom f1 by A7,Th1;
A14: rng s c=right_open_halfline(x0) by A7,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A15:  q.n=x by FUNCT_2:113;
A16:   n+k in NAT by ORDINAL1:def 12;
A17:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108,A16
        .=x by A15,NAT_1:def 3;
A18:  s.(n+k)<x0+g by A8,NAT_1:12;
A19:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in right_open_halfline(x0) by A14;
      then s.(n+k) in {g1: x0<g1} by XXREAL_1:230;
      then ex g1 st g1=s.(n+k) & x0<g1;
      then s.(n+k) in {g2: x0<g2 & g2<x0+g} by A18;
      then s.(n+k) in ].x0,x0+g.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0,x0+g.[ by A13,A19,XBOOLE_0:def 4;
      then lim_right(f1,x0)<f1.(s.(n+k)) by A5;
      then f1.(s.(n+k)) in {r1: lim_right(f1,x0)<r1};
      then
A20:  f1.(s.(n+k)) in right_open_halfline(lim_right(f1,x0)) by XXREAL_1:230;
      f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11;
      hence x in dom f2/\right_open_halfline(lim_right(f1,x0)) by A20,A17,
XBOOLE_0:def 4;
    end;
    then
A21: rng q c=dom f2/\ right_open_halfline(lim_right(f1,x0));
    lim(f1/*s)=lim_right(f1,x0) by A1,A6,A11,LIMFUNC2:def 8;
    then lim q=lim_right(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to-infty by A2,A12,A21,LIMFUNC2:def 6;
    hence (f2*f1)/*s is divergent_to-infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC2:def 6;
end;

theorem
  f1 is_right_convergent_in x0 & f2 is_left_divergent_to+infty_in
lim_right(f1,x0) & (for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1)) & (ex g
  st 0<g & for r st r in dom f1 /\ ].x0,x0+g.[ holds f1.r<lim_right(f1,x0))
  implies f2*f1 is_right_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_left_divergent_to+infty_in lim_right(f1,x0) and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0,x0+g.[ holds f1.r<lim_right(f1,x0);
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)/\right_open_halfline(x0);
    consider k be Nat such that
A8: for n be Nat st k<=n holds s.n<x0+g by A4,A6,Lm1,LIMFUNC2:2;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th1;
    rng(f1/*s)c=dom f2 by A7,Th1;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1/\right_open_halfline(x0) by A7,Th1;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC2:def 8;
A13: rng s c=dom f1 by A7,Th1;
A14: rng s c=right_open_halfline(x0) by A7,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A15:  q.n=x by FUNCT_2:113;
A16:   n+k in NAT by ORDINAL1:def 12;
A17:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108,A16
        .=x by A15,NAT_1:def 3;
A18:  s.(n+k)<x0+g by A8,NAT_1:12;
A19:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in right_open_halfline(x0) by A14;
      then s.(n+k) in {g1: x0<g1} by XXREAL_1:230;
      then ex g1 st g1=s.(n+k) & x0<g1;
      then s.(n+k) in {g2: x0<g2 & g2<x0+g} by A18;
      then s.(n+k) in ].x0,x0+g.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0,x0+g.[ by A13,A19,XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim_right(f1,x0) by A5;
      then f1.(s.(n+k)) in {r1: r1<lim_right(f1,x0)};
      then
A20:  f1.(s.(n+k)) in left_open_halfline(lim_right(f1,x0)) by XXREAL_1:229;
      f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11;
      hence x in dom f2/\left_open_halfline(lim_right(f1,x0)) by A20,A17,
XBOOLE_0:def 4;
    end;
    then
A21: rng q c=dom f2/\left_open_halfline(lim_right(f1,x0));
    lim(f1/*s)=lim_right(f1,x0) by A1,A6,A11,LIMFUNC2:def 8;
    then lim q=lim_right(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to+infty by A2,A12,A21,LIMFUNC2:def 2;
    hence (f2*f1)/*s is divergent_to+infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC2:def 5;
end;

theorem
  f1 is_right_convergent_in x0 & f2 is_left_divergent_to-infty_in
lim_right(f1,x0) & (for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1)) & (ex g
  st 0<g & for r st r in dom f1 /\ ].x0,x0+g.[ holds f1.r<lim_right(f1,x0))
  implies f2*f1 is_right_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_left_divergent_to-infty_in lim_right(f1,x0) and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0,x0+g.[ holds f1.r<lim_right(f1,x0);
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)/\right_open_halfline(x0);
    consider k be Nat such that
A8: for n be Nat st k<=n holds s.n<x0+g by A4,A6,Lm1,LIMFUNC2:2;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th1;
    rng(f1/*s)c=dom f2 by A7,Th1;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1/\right_open_halfline(x0) by A7,Th1;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC2:def 8;
A13: rng s c=dom f1 by A7,Th1;
A14: rng s c=right_open_halfline(x0) by A7,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A15:  q.n=x by FUNCT_2:113;
A16:   n+k in NAT by ORDINAL1:def 12;
A17:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108,A16
        .=x by A15,NAT_1:def 3;
A18:  s.(n+k)<x0+g by A8,NAT_1:12;
A19:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in right_open_halfline(x0) by A14;
      then s.(n+k) in {g1: x0<g1} by XXREAL_1:230;
      then ex g1 st g1=s.(n+k) & x0<g1;
      then s.(n+k) in {g2: x0<g2 & g2<x0+g} by A18;
      then s.(n+k) in ].x0,x0+g.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0,x0+g.[ by A13,A19,XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim_right(f1,x0) by A5;
      then f1.(s.(n+k)) in {r1: r1<lim_right(f1,x0)};
      then
A20:  f1.(s.(n+k)) in left_open_halfline(lim_right(f1,x0)) by XXREAL_1:229;
      f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11;
      hence x in dom f2/\left_open_halfline(lim_right(f1,x0)) by A20,A17,
XBOOLE_0:def 4;
    end;
    then
A21: rng q c=dom f2/\left_open_halfline(lim_right(f1,x0));
    lim(f1/*s)=lim_right(f1,x0) by A1,A6,A11,LIMFUNC2:def 8;
    then lim q=lim_right(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to-infty by A2,A12,A21,LIMFUNC2:def 3;
    hence (f2*f1)/*s is divergent_to-infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC2:def 6;
end;

theorem
  f1 is convergent_in+infty & f2 is_left_divergent_to+infty_in
  lim_in+infty f1 & (for r ex g st r<g & g in dom(f2*f1)) & (ex r st for g st g
  in dom f1 /\ right_open_halfline(r) holds f1.g<lim_in+infty f1) implies f2*f1
  is divergent_in+infty_to+infty
proof
  assume that
A1: f1 is convergent_in+infty and
A2: f2 is_left_divergent_to+infty_in lim_in+infty f1 and
A3: for r ex g st r<g & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\right_open_halfline(r) holds f1.g<lim_in+infty f1;
  now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to+infty and
A6: rng s c=dom(f2*f1);
    consider k be Nat such that
A7: for n be Nat st k<=n holds r<s.n by A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    set q=s^\k;
A9: q is divergent_to+infty by A5,LIMFUNC1:26;
A10: rng s c=dom f1 by A6,Lm2;
A11: rng q c=rng s by VALUED_0:21;
A12: rng(f1/*q)c=dom f2/\left_open_halfline(lim_in+infty f1)
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A13:  (f1/*q).n=x by FUNCT_2:113;
A14:  x=f1.(q.n) by A10,A11,A13,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      r<s.(n+k) by A7,NAT_1:12;
      then s.(n+k) in {r2: r<r2};
      then
A15:  s.(n+k) in right_open_halfline(r) by XXREAL_1:230;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\right_open_halfline(r) by A10,A15,XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim_in+infty f1 by A4;
      then x in {g1: g1<lim_in+infty f1} by A14;
      then
A16:  x in left_open_halfline(lim_in+infty f1) by XXREAL_1:229;
A17:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A8;
      then x in dom f2 by A10,A14,FUNCT_2:108,A17;
      hence thesis by A16,XBOOLE_0:def 4;
    end;
    rng q c=dom f1 by A10,A11;
    then f1/*q is convergent & lim(f1/*q)=lim_in+infty f1 by A1,A9,
LIMFUNC1:def 12;
    then
A18: f2/*(f1/*q) is divergent_to+infty by A2,A12,LIMFUNC2:def 2;
    f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A8,VALUED_0:27
      .=((f2*f1)/*s)^\k by A6,VALUED_0:31;
    hence (f2*f1)/*s is divergent_to+infty by A18,LIMFUNC1:7;
  end;
  hence thesis by A3;
end;

theorem
  f1 is convergent_in+infty & f2 is_left_divergent_to-infty_in
  lim_in+infty f1 & (for r ex g st r<g & g in dom(f2*f1)) & (ex r st for g st g
  in dom f1 /\ right_open_halfline(r) holds f1.g<lim_in+infty f1) implies f2*f1
  is divergent_in+infty_to-infty
proof
  assume that
A1: f1 is convergent_in+infty and
A2: f2 is_left_divergent_to-infty_in lim_in+infty f1 and
A3: for r ex g st r<g & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\right_open_halfline(r) holds f1.g<lim_in+infty f1;
  now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to+infty and
A6: rng s c=dom(f2*f1);
    consider k be Nat such that
A7: for n be Nat st k<=n holds r<s.n by A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    set q=s^\k;
A9: q is divergent_to+infty by A5,LIMFUNC1:26;
A10: rng s c=dom f1 by A6,Lm2;
A11: rng q c=rng s by VALUED_0:21;
A12: rng(f1/*q)c=dom f2/\left_open_halfline(lim_in+infty f1)
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A13:  (f1/*q).n=x by FUNCT_2:113;
A14:  x=f1.(q.n) by A10,A11,A13,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      r<s.(n+k) by A7,NAT_1:12;
      then s.(n+k) in {r2: r<r2};
      then
A15:  s.(n+k) in right_open_halfline(r) by XXREAL_1:230;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\right_open_halfline(r) by A10,A15,XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim_in+infty f1 by A4;
      then x in {g1: g1<lim_in+infty f1} by A14;
      then
A16:  x in left_open_halfline(lim_in+infty f1) by XXREAL_1:229;
A17:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A8;
      then x in dom f2 by A10,A14,FUNCT_2:108,A17;
      hence thesis by A16,XBOOLE_0:def 4;
    end;
    rng q c=dom f1 by A10,A11;
    then f1/*q is convergent & lim(f1/*q)=lim_in+infty f1 by A1,A9,
LIMFUNC1:def 12;
    then
A18: f2/*(f1/*q) is divergent_to-infty by A2,A12,LIMFUNC2:def 3;
    f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A8,VALUED_0:27
      .=((f2*f1)/*s)^\k by A6,VALUED_0:31;
    hence (f2*f1)/*s is divergent_to-infty by A18,LIMFUNC1:7;
  end;
  hence thesis by A3;
end;

theorem
  f1 is convergent_in+infty & f2 is_right_divergent_to+infty_in
  lim_in+infty f1 & (for r ex g st r<g & g in dom(f2*f1)) & (ex r st for g st g
  in dom f1 /\ right_open_halfline(r) holds lim_in+infty f1<f1.g) implies f2*f1
  is divergent_in+infty_to+infty
proof
  assume that
A1: f1 is convergent_in+infty and
A2: f2 is_right_divergent_to+infty_in lim_in+infty f1 and
A3: for r ex g st r<g & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\right_open_halfline(r) holds lim_in+infty f1< f1.g;
  now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to+infty and
A6: rng s c=dom(f2*f1);
    consider k be Nat such that
A7: for n be Nat st k<=n holds r<s.n by A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    set q=s^\k;
A9: q is divergent_to+infty by A5,LIMFUNC1:26;
A10: rng s c=dom f1 by A6,Lm2;
A11: rng q c=rng s by VALUED_0:21;
A12: rng(f1/*q)c=dom f2/\right_open_halfline(lim_in+infty f1)
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A13:  (f1/*q).n=x by FUNCT_2:113;
A14:  x=f1.(q.n) by A10,A11,A13,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      r<s.(n+k) by A7,NAT_1:12;
      then s.(n+k) in {r2: r<r2};
      then
A15:  s.(n+k) in right_open_halfline(r) by XXREAL_1:230;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\right_open_halfline(r) by A10,A15,XBOOLE_0:def 4;
      then lim_in+infty f1<f1.(s.(n+k)) by A4;
      then x in {g1: lim_in+infty f1<g1} by A14;
      then
A16:  x in right_open_halfline(lim_in+infty f1) by XXREAL_1:230;
A17:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A8;
      then x in dom f2 by A10,A14,FUNCT_2:108,A17;
      hence thesis by A16,XBOOLE_0:def 4;
    end;
    rng q c=dom f1 by A10,A11;
    then f1/*q is convergent & lim(f1/*q)=lim_in+infty f1 by A1,A9,
LIMFUNC1:def 12;
    then
A18: f2/*(f1/*q) is divergent_to+infty by A2,A12,LIMFUNC2:def 5;
    f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A8,VALUED_0:27
      .=((f2*f1)/*s)^\k by A6,VALUED_0:31;
    hence (f2*f1)/*s is divergent_to+infty by A18,LIMFUNC1:7;
  end;
  hence thesis by A3;
end;

theorem
  f1 is convergent_in+infty & f2 is_right_divergent_to-infty_in
  lim_in+infty f1 & (for r ex g st r<g & g in dom(f2*f1)) & (ex r st for g st g
  in dom f1 /\ right_open_halfline(r) holds lim_in+infty f1<f1.g) implies f2*f1
  is divergent_in+infty_to-infty
proof
  assume that
A1: f1 is convergent_in+infty and
A2: f2 is_right_divergent_to-infty_in lim_in+infty f1 and
A3: for r ex g st r<g & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\right_open_halfline(r) holds lim_in+infty f1< f1.g;
  now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to+infty and
A6: rng s c=dom(f2*f1);
    consider k be Nat such that
A7: for n be Nat st k<=n holds r<s.n by A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    set q=s^\k;
A9: q is divergent_to+infty by A5,LIMFUNC1:26;
A10: rng s c=dom f1 by A6,Lm2;
A11: rng q c=rng s by VALUED_0:21;
A12: rng(f1/*q)c=dom f2/\right_open_halfline(lim_in+infty f1)
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A13:  (f1/*q).n=x by FUNCT_2:113;
A14:  x=f1.(q.n) by A10,A11,A13,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      r<s.(n+k) by A7,NAT_1:12;
      then s.(n+k) in {r2: r<r2};
      then
A15:  s.(n+k) in right_open_halfline(r) by XXREAL_1:230;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\right_open_halfline(r) by A10,A15,XBOOLE_0:def 4;
      then lim_in+infty f1<f1.(s.(n+k)) by A4;
      then x in {g1: lim_in+infty f1<g1} by A14;
      then
A16:  x in right_open_halfline(lim_in+infty f1) by XXREAL_1:230;
A17:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A8;
      then x in dom f2 by A10,A14,FUNCT_2:108,A17;
      hence thesis by A16,XBOOLE_0:def 4;
    end;
    rng q c=dom f1 by A10,A11;
    then f1/*q is convergent & lim(f1/*q)=lim_in+infty f1 by A1,A9,
LIMFUNC1:def 12;
    then
A18: f2/*(f1/*q) is divergent_to-infty by A2,A12,LIMFUNC2:def 6;
    f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A8,VALUED_0:27
      .=((f2*f1)/*s)^\k by A6,VALUED_0:31;
    hence (f2*f1)/*s is divergent_to-infty by A18,LIMFUNC1:7;
  end;
  hence thesis by A3;
end;

theorem
  f1 is convergent_in-infty & f2 is_left_divergent_to+infty_in
  lim_in-infty f1 & (for r ex g st g<r & g in dom(f2*f1)) & (ex r st for g st g
in dom f1 /\ left_open_halfline(r) holds f1.g<lim_in-infty f1) implies f2*f1 is
  divergent_in-infty_to+infty
proof
  assume that
A1: f1 is convergent_in-infty and
A2: f2 is_left_divergent_to+infty_in lim_in-infty f1 and
A3: for r ex g st g<r & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\left_open_halfline(r) holds f1.g<lim_in-infty f1;
  now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to-infty and
A6: rng s c=dom(f2*f1);
    consider k be Nat such that
A7: for n be Nat st k<=n holds s.n<r by A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    set q=s^\k;
A9: q is divergent_to-infty by A5,LIMFUNC1:27;
A10: rng s c=dom f1 by A6,Lm2;
A11: rng q c=rng s by VALUED_0:21;
A12: rng(f1/*q)c=dom f2/\left_open_halfline(lim_in-infty f1)
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A13:  (f1/*q).n=x by FUNCT_2:113;
A14:  x=f1.(q.n) by A10,A11,A13,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      s.(n+k)<r by A7,NAT_1:12;
      then s.(n+k) in {r2: r2<r};
      then
A15:  s.(n+k) in left_open_halfline(r) by XXREAL_1:229;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\left_open_halfline(r) by A10,A15,XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim_in-infty f1 by A4;
      then x in {g1: g1<lim_in-infty f1} by A14;
      then
A16:  x in left_open_halfline(lim_in-infty f1) by XXREAL_1:229;
A17:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A8;
      then x in dom f2 by A10,A14,FUNCT_2:108,A17;
      hence thesis by A16,XBOOLE_0:def 4;
    end;
    rng q c=dom f1 by A10,A11;
    then f1/*q is convergent & lim(f1/*q)=lim_in-infty f1 by A1,A9,
LIMFUNC1:def 13;
    then
A18: f2/*(f1/*q) is divergent_to+infty by A2,A12,LIMFUNC2:def 2;
    f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A8,VALUED_0:27
      .=((f2*f1)/*s)^\k by A6,VALUED_0:31;
    hence (f2*f1)/*s is divergent_to+infty by A18,LIMFUNC1:7;
  end;
  hence thesis by A3;
end;

theorem
  f1 is convergent_in-infty & f2 is_left_divergent_to-infty_in
  lim_in-infty f1 & (for r ex g st g<r & g in dom(f2*f1)) & (ex r st for g st g
in dom f1 /\ left_open_halfline(r) holds f1.g<lim_in-infty f1) implies f2*f1 is
  divergent_in-infty_to-infty
proof
  assume that
A1: f1 is convergent_in-infty and
A2: f2 is_left_divergent_to-infty_in lim_in-infty f1 and
A3: for r ex g st g<r & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\left_open_halfline(r) holds f1.g<lim_in-infty f1;
  now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to-infty and
A6: rng s c=dom(f2*f1);
    consider k be Nat such that
A7: for n be Nat st k<=n holds s.n<r by A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    set q=s^\k;
A9: q is divergent_to-infty by A5,LIMFUNC1:27;
A10: rng s c=dom f1 by A6,Lm2;
A11: rng q c=rng s by VALUED_0:21;
A12: rng(f1/*q)c=dom f2/\left_open_halfline(lim_in-infty f1)
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A13:  (f1/*q).n=x by FUNCT_2:113;
A14:  x=f1.(q.n) by A10,A11,A13,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      s.(n+k)<r by A7,NAT_1:12;
      then s.(n+k) in {r2: r2<r};
      then
A15:  s.(n+k) in left_open_halfline(r) by XXREAL_1:229;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\left_open_halfline(r) by A10,A15,XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim_in-infty f1 by A4;
      then x in {g1: g1<lim_in-infty f1} by A14;
      then
A16:  x in left_open_halfline(lim_in-infty f1) by XXREAL_1:229;
A17:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A8;
      then x in dom f2 by A10,A14,FUNCT_2:108,A17;
      hence thesis by A16,XBOOLE_0:def 4;
    end;
    rng q c=dom f1 by A10,A11;
    then f1/*q is convergent & lim(f1/*q)=lim_in-infty f1 by A1,A9,
LIMFUNC1:def 13;
    then
A18: f2/*(f1/*q) is divergent_to-infty by A2,A12,LIMFUNC2:def 3;
    f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A8,VALUED_0:27
      .=((f2*f1)/*s)^\k by A6,VALUED_0:31;
    hence (f2*f1)/*s is divergent_to-infty by A18,LIMFUNC1:7;
  end;
  hence thesis by A3;
end;

theorem
  f1 is convergent_in-infty & f2 is_right_divergent_to+infty_in
  lim_in-infty f1 & (for r ex g st g<r & g in dom(f2*f1)) & (ex r st for g st g
in dom f1 /\ left_open_halfline(r) holds lim_in-infty f1<f1.g) implies f2*f1 is
  divergent_in-infty_to+infty
proof
  assume that
A1: f1 is convergent_in-infty and
A2: f2 is_right_divergent_to+infty_in lim_in-infty f1 and
A3: for r ex g st g<r & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\left_open_halfline(r) holds lim_in-infty f1<f1 .g;
  now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to-infty and
A6: rng s c=dom(f2*f1);
    consider k be Nat such that
A7: for n be Nat st k<=n holds s.n<r by A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    set q=s^\k;
A9: q is divergent_to-infty by A5,LIMFUNC1:27;
A10: rng s c=dom f1 by A6,Lm2;
A11: rng q c=rng s by VALUED_0:21;
A12: rng(f1/*q)c=dom f2/\right_open_halfline(lim_in-infty f1)
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A13:  (f1/*q).n=x by FUNCT_2:113;
A14:  x=f1.(q.n) by A10,A11,A13,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      s.(n+k)<r by A7,NAT_1:12;
      then s.(n+k) in {r2: r2<r};
      then
A15:  s.(n+k) in left_open_halfline(r) by XXREAL_1:229;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\left_open_halfline(r) by A10,A15,XBOOLE_0:def 4;
      then lim_in-infty f1<f1.(s.(n+k)) by A4;
      then x in {g1: lim_in-infty f1<g1} by A14;
      then
A16:  x in right_open_halfline(lim_in-infty f1) by XXREAL_1:230;
A17:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A8;
      then x in dom f2 by A10,A14,FUNCT_2:108,A17;
      hence thesis by A16,XBOOLE_0:def 4;
    end;
    rng q c=dom f1 by A10,A11;
    then f1/*q is convergent & lim(f1/*q)=lim_in-infty f1 by A1,A9,
LIMFUNC1:def 13;
    then
A18: f2/*(f1/*q) is divergent_to+infty by A2,A12,LIMFUNC2:def 5;
    f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A8,VALUED_0:27
      .=((f2*f1)/*s)^\k by A6,VALUED_0:31;
    hence (f2*f1)/*s is divergent_to+infty by A18,LIMFUNC1:7;
  end;
  hence thesis by A3;
end;

theorem
  f1 is convergent_in-infty & f2 is_right_divergent_to-infty_in
  lim_in-infty f1 & (for r ex g st g<r & g in dom(f2*f1)) & (ex r st for g st g
in dom f1 /\ left_open_halfline(r) holds lim_in-infty f1<f1.g) implies f2*f1 is
  divergent_in-infty_to-infty
proof
  assume that
A1: f1 is convergent_in-infty and
A2: f2 is_right_divergent_to-infty_in lim_in-infty f1 and
A3: for r ex g st g<r & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\left_open_halfline(r) holds lim_in-infty f1<f1 .g;
  now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to-infty and
A6: rng s c=dom(f2*f1);
    consider k be Nat such that
A7: for n be Nat st k<=n holds s.n<r by A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    set q=s^\k;
A9: q is divergent_to-infty by A5,LIMFUNC1:27;
A10: rng s c=dom f1 by A6,Lm2;
A11: rng q c=rng s by VALUED_0:21;
A12: rng(f1/*q)c=dom f2/\right_open_halfline(lim_in-infty f1)
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A13:  (f1/*q).n=x by FUNCT_2:113;
A14:  x=f1.(q.n) by A10,A11,A13,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      s.(n+k)<r by A7,NAT_1:12;
      then s.(n+k) in {r2: r2<r};
      then
A15:  s.(n+k) in left_open_halfline(r) by XXREAL_1:229;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\left_open_halfline(r) by A10,A15,XBOOLE_0:def 4;
      then lim_in-infty f1<f1.(s.(n+k)) by A4;
      then x in {g1: lim_in-infty f1<g1} by A14;
      then
A16:  x in right_open_halfline(lim_in-infty f1) by XXREAL_1:230;
A17:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A8;
      then x in dom f2 by A10,A14,FUNCT_2:108,A17;
      hence thesis by A16,XBOOLE_0:def 4;
    end;
    rng q c=dom f1 by A10,A11;
    then f1/*q is convergent & lim(f1/*q)=lim_in-infty f1 by A1,A9,
LIMFUNC1:def 13;
    then
A18: f2/*(f1/*q) is divergent_to-infty by A2,A12,LIMFUNC2:def 6;
    f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A8,VALUED_0:27
      .=((f2*f1)/*s)^\k by A6,VALUED_0:31;
    hence (f2*f1)/*s is divergent_to-infty by A18,LIMFUNC1:7;
  end;
  hence thesis by A3;
end;

theorem
  f1 is_divergent_to+infty_in x0 & f2 is divergent_in+infty_to+infty & (
for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2<r2
  & x0<g2 & g2 in dom(f2*f1)) implies f2*f1 is_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_divergent_to+infty_in x0 and
A2: f2 is divergent_in+infty_to+infty and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is convergent & lim s=x0 and
A5: rng s c=dom(f2*f1)\{x0};
A6: rng s c=dom(f2*f1) by A5,Th2;
    rng s c=dom f1\{x0} by A5,Th2;
    then
A7: f1/*s is divergent_to+infty by A1,A4,LIMFUNC3:def 2;
    rng(f1/*s)c=dom f2 by A5,Th2;
    then f2/*(f1/*s) is divergent_to+infty by A2,A7;
    hence (f2*f1)/*s is divergent_to+infty by A6,VALUED_0:31;
  end;
  hence thesis by A3,LIMFUNC3:def 2;
end;

theorem
  f1 is_divergent_to+infty_in x0 & f2 is divergent_in+infty_to-infty & (
for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2<r2
  & x0<g2 & g2 in dom(f2*f1)) implies f2*f1 is_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_divergent_to+infty_in x0 and
A2: f2 is divergent_in+infty_to-infty and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is convergent & lim s=x0 and
A5: rng s c=dom(f2*f1)\{x0};
A6: rng s c=dom(f2*f1) by A5,Th2;
    rng s c=dom f1\{x0} by A5,Th2;
    then
A7: f1/*s is divergent_to+infty by A1,A4,LIMFUNC3:def 2;
    rng(f1/*s)c=dom f2 by A5,Th2;
    then f2/*(f1/*s) is divergent_to-infty by A2,A7;
    hence (f2*f1)/*s is divergent_to-infty by A6,VALUED_0:31;
  end;
  hence thesis by A3,LIMFUNC3:def 3;
end;

theorem
  f1 is_divergent_to-infty_in x0 & f2 is divergent_in-infty_to+infty & (
for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2<r2
  & x0<g2 & g2 in dom(f2*f1)) implies f2*f1 is_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_divergent_to-infty_in x0 and
A2: f2 is divergent_in-infty_to+infty and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is convergent & lim s=x0 and
A5: rng s c=dom(f2*f1)\{x0};
A6: rng s c=dom(f2*f1) by A5,Th2;
    rng s c=dom f1\{x0} by A5,Th2;
    then
A7: f1/*s is divergent_to-infty by A1,A4,LIMFUNC3:def 3;
    rng(f1/*s)c=dom f2 by A5,Th2;
    then f2/*(f1/*s) is divergent_to+infty by A2,A7;
    hence (f2*f1)/*s is divergent_to+infty by A6,VALUED_0:31;
  end;
  hence thesis by A3,LIMFUNC3:def 2;
end;

theorem
  f1 is_divergent_to-infty_in x0 & f2 is divergent_in-infty_to-infty & (
for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2<r2
  & x0<g2 & g2 in dom(f2*f1)) implies f2*f1 is_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_divergent_to-infty_in x0 and
A2: f2 is divergent_in-infty_to-infty and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
  now
    let s be Real_Sequence;
    assume that
A4: s is convergent & lim s=x0 and
A5: rng s c=dom(f2*f1)\{x0};
A6: rng s c=dom(f2*f1) by A5,Th2;
    rng s c=dom f1\{x0} by A5,Th2;
    then
A7: f1/*s is divergent_to-infty by A1,A4,LIMFUNC3:def 3;
    rng(f1/*s)c=dom f2 by A5,Th2;
    then f2/*(f1/*s) is divergent_to-infty by A2,A7;
    hence (f2*f1)/*s is divergent_to-infty by A6,VALUED_0:31;
  end;
  hence thesis by A3,LIMFUNC3:def 3;
end;

theorem
  f1 is_convergent_in x0 & f2 is_divergent_to+infty_in lim(f1,x0) & (for
  r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2<r2 &
x0<g2 & g2 in dom(f2*f1)) & (ex g st 0<g & for r st r in dom f1 /\ (].x0-g,x0.[
\/ ].x0,x0+g.[) holds f1.r<>lim(f1,x0)) implies f2*f1 is_divergent_to+infty_in
  x0
proof
  assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_divergent_to+infty_in lim(f1,x0) and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) holds f1.r<>lim(f1, x0);
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)\{x0};
    consider k be Element of NAT such that
A8: for n being Element of NAT st k<=n holds x0-g<s.n & s.n<x0+g by A4,A6,
LIMFUNC3:7;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th2;
    rng(f1/*s)c=dom f2 by A7,Th2;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1\{x0} by A7,Th2;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC3:def 4;
A13: rng s c=dom f1 by A7,Th2;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A14:  q.n=x by FUNCT_2:113;
A15:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108
        .=x by A14,NAT_1:def 3;
      k<=n+k by NAT_1:12;
      then x0-g<s.(n+k) & s.(n+k)<x0+g by A8;
      then s.(n+k) in {g1: x0-g<g1 & g1<x0+g};
      then
A16:  s.(n+k) in ].x0-g,x0+g.[ by RCOMP_1:def 2;
A17:  s.(n+k) in rng s by VALUED_0:28;
      then not s.(n+k) in {x0} by A7,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0+g.[\{x0} by A16,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0.[\/].x0,x0+g.[ by A4,LIMFUNC3:4;
      then s.(n+k) in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) by A13,A17,
XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim(f1,x0) by A5;
      then
A18:  not f1.(s.(n+k)) in {lim(f1,x0)} by TARSKI:def 1;
      f1.(s.(n+k)) in dom f2 by A9,A17,FUNCT_1:11;
      hence x in dom f2\{lim(f1,x0)} by A18,A15,XBOOLE_0:def 5;
    end;
    then
A19: rng q c=dom f2\{lim(f1,x0)};
    lim(f1/*s)=lim(f1,x0) by A1,A6,A11,LIMFUNC3:def 4;
    then lim q=lim(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to+infty by A2,A12,A19,LIMFUNC3:def 2;
    hence (f2*f1)/*s is divergent_to+infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC3:def 2;
end;

theorem
  f1 is_convergent_in x0 & f2 is_divergent_to-infty_in lim(f1,x0) & (for
  r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2<r2 &
x0<g2 & g2 in dom(f2*f1)) & (ex g st 0<g & for r st r in dom f1 /\ (].x0-g,x0.[
\/ ].x0,x0+g.[) holds f1.r<>lim(f1,x0)) implies f2*f1 is_divergent_to-infty_in
  x0
proof
  assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_divergent_to-infty_in lim(f1,x0) and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) holds f1.r<>lim(f1, x0);
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)\{x0};
    consider k be Element of NAT such that
A8: for n being Element of NAT st k<=n holds x0-g<s.n & s.n<x0+g by A4,A6,
LIMFUNC3:7;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th2;
    rng(f1/*s)c=dom f2 by A7,Th2;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1\{x0} by A7,Th2;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC3:def 4;
A13: rng s c=dom f1 by A7,Th2;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A14:  q.n=x by FUNCT_2:113;
A15:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108
        .=x by A14,NAT_1:def 3;
      k<=n+k by NAT_1:12;
      then x0-g<s.(n+k) & s.(n+k)<x0+g by A8;
      then s.(n+k) in {g1: x0-g<g1 & g1<x0+g};
      then
A16:  s.(n+k) in ].x0-g,x0+g.[ by RCOMP_1:def 2;
A17:  s.(n+k) in rng s by VALUED_0:28;
      then not s.(n+k) in {x0} by A7,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0+g.[\{x0} by A16,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0.[\/].x0,x0+g.[ by A4,LIMFUNC3:4;
      then s.(n+k) in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) by A13,A17,
XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim(f1,x0) by A5;
      then
A18:  not f1.(s.(n+k)) in {lim(f1,x0)} by TARSKI:def 1;
      f1.(s.(n+k)) in dom f2 by A9,A17,FUNCT_1:11;
      hence x in dom f2\{lim(f1,x0)} by A18,A15,XBOOLE_0:def 5;
    end;
    then
A19: rng q c=dom f2\{lim(f1,x0)};
    lim(f1/*s)=lim(f1,x0) by A1,A6,A11,LIMFUNC3:def 4;
    then lim q=lim(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to-infty by A2,A12,A19,LIMFUNC3:def 3;
    hence (f2*f1)/*s is divergent_to-infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC3:def 3;
end;

theorem
  f1 is_convergent_in x0 & f2 is_right_divergent_to+infty_in lim(f1,x0)
& (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2
<r2 & x0<g2 & g2 in dom(f2*f1)) & (ex g st 0<g & for r st r in dom f1 /\ (].x0-
  g,x0.[ \/ ].x0,x0+g.[) holds f1.r>lim(f1,x0)) implies f2*f1
  is_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_right_divergent_to+infty_in lim(f1,x0) and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) holds lim(f1,x0)<f1 .r;
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)\{x0};
    consider k be Element of NAT such that
A8: for n being Element of NAT st k<=n holds x0-g<s.n & s.n<x0+g by A4,A6,
LIMFUNC3:7;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th2;
    rng(f1/*s)c=dom f2 by A7,Th2;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1\{x0} by A7,Th2;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC3:def 4;
A13: rng s c=dom f1 by A7,Th2;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A14:  q.n=x by FUNCT_2:113;
A15:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108
        .=x by A14,NAT_1:def 3;
      k<=n+k by NAT_1:12;
      then x0-g<s.(n+k) & s.(n+k)<x0+g by A8;
      then s.(n+k) in {g1: x0-g<g1 & g1<x0+g};
      then
A16:  s.(n+k) in ].x0-g,x0+g.[ by RCOMP_1:def 2;
A17:  s.(n+k) in rng s by VALUED_0:28;
      then not s.(n+k) in {x0} by A7,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0+g.[\{x0} by A16,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0.[\/].x0,x0+g.[ by A4,LIMFUNC3:4;
      then s.(n+k) in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) by A13,A17,
XBOOLE_0:def 4;
      then f1.(s.(n+k))>lim(f1,x0) by A5;
      then f1.(s.(n+k)) in {g2: lim(f1,x0)<g2};
      then
A18:  f1.(s.(n+k)) in right_open_halfline(lim(f1,x0)) by XXREAL_1:230;
      f1.(s.(n+k)) in dom f2 by A9,A17,FUNCT_1:11;
      hence x in dom f2/\right_open_halfline(lim(f1,x0)) by A18,A15,
XBOOLE_0:def 4;
    end;
    then
A19: rng q c=dom f2/\right_open_halfline(lim(f1,x0));
    lim(f1/*s)=lim(f1,x0) by A1,A6,A11,LIMFUNC3:def 4;
    then lim q=lim(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to+infty by A2,A12,A19,LIMFUNC2:def 5;
    hence (f2*f1)/*s is divergent_to+infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC3:def 2;
end;

theorem
  f1 is_convergent_in x0 & f2 is_right_divergent_to-infty_in lim(f1,x0)
& (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2
<r2 & x0<g2 & g2 in dom(f2*f1)) & (ex g st 0<g & for r st r in dom f1 /\ (].x0-
  g,x0.[ \/ ].x0,x0+g.[) holds f1.r>lim(f1,x0)) implies f2*f1
  is_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_right_divergent_to-infty_in lim(f1,x0) and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) holds lim(f1,x0)<f1 .r;
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)\{x0};
    consider k be Element of NAT such that
A8: for n being Element of NAT st k<=n holds x0-g<s.n & s.n<x0+g by A4,A6,
LIMFUNC3:7;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th2;
    rng(f1/*s)c=dom f2 by A7,Th2;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1\{x0} by A7,Th2;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC3:def 4;
A13: rng s c=dom f1 by A7,Th2;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A14:  q.n=x by FUNCT_2:113;
A15:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108
        .=x by A14,NAT_1:def 3;
      k<=n+k by NAT_1:12;
      then x0-g<s.(n+k) & s.(n+k)<x0+g by A8;
      then s.(n+k) in {g1: x0-g<g1 & g1<x0+g};
      then
A16:  s.(n+k) in ].x0-g,x0+g.[ by RCOMP_1:def 2;
A17:  s.(n+k) in rng s by VALUED_0:28;
      then not s.(n+k) in {x0} by A7,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0+g.[\{x0} by A16,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0.[\/].x0,x0+g.[ by A4,LIMFUNC3:4;
      then s.(n+k) in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) by A13,A17,
XBOOLE_0:def 4;
      then f1.(s.(n+k))>lim(f1,x0) by A5;
      then f1.(s.(n+k)) in {g2: lim(f1,x0)<g2};
      then
A18:  f1.(s.(n+k)) in right_open_halfline(lim(f1,x0)) by XXREAL_1:230;
      f1.(s.(n+k)) in dom f2 by A9,A17,FUNCT_1:11;
      hence x in dom f2/\right_open_halfline(lim(f1,x0)) by A18,A15,
XBOOLE_0:def 4;
    end;
    then
A19: rng q c=dom f2/\right_open_halfline(lim(f1,x0));
    lim(f1/*s)=lim(f1,x0) by A1,A6,A11,LIMFUNC3:def 4;
    then lim q=lim(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to-infty by A2,A12,A19,LIMFUNC2:def 6;
    hence (f2*f1)/*s is divergent_to-infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC3:def 3;
end;

theorem
  f1 is_right_convergent_in x0 & f2 is_divergent_to+infty_in lim_right(
f1,x0 ) & (for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1)) & (ex g st 0<g &
for r st r in dom f1 /\ ].x0,x0+g.[ holds f1.r<>lim_right(f1,x0)) implies f2*f1
  is_right_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_divergent_to+infty_in lim_right(f1,x0) and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0,x0+g.[ holds f1.r<>lim_right(f1,x0);
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)/\right_open_halfline(x0);
    consider k be Nat such that
A8: for n be Nat st k<=n holds s.n<x0+g by A4,A6,Lm1,LIMFUNC2:2;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th1;
    rng(f1/*s)c=dom f2 by A7,Th1;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1/\right_open_halfline(x0) by A7,Th1;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC2:def 8;
A13: rng s c=dom f1 by A7,Th1;
A14: rng s c=right_open_halfline(x0) by A7,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A15:  q.n=x by FUNCT_2:113;
A16:   n+k in NAT by ORDINAL1:def 12;
A17:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108,A16
        .=x by A15,NAT_1:def 3;
A18:  s.(n+k)<x0+g by A8,NAT_1:12;
A19:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in right_open_halfline(x0) by A14;
      then s.(n+k) in {g1: x0<g1} by XXREAL_1:230;
      then ex g1 st g1=s.(n+k) & x0<g1;
      then s.(n+k) in {g2: x0<g2 & g2<x0+g} by A18;
      then s.(n+k) in ].x0,x0+g.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0,x0+g.[ by A13,A19,XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim_right(f1,x0) by A5;
      then
A20:  not f1.(s.(n+k)) in {lim_right(f1,x0)} by TARSKI:def 1;
      f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11;
      hence x in dom f2\{lim_right(f1,x0)} by A20,A17,XBOOLE_0:def 5;
    end;
    then
A21: rng q c=dom f2\{lim_right(f1,x0)};
    lim(f1/*s)=lim_right(f1,x0) by A1,A6,A11,LIMFUNC2:def 8;
    then lim q=lim_right(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to+infty by A2,A12,A21,LIMFUNC3:def 2;
    hence (f2*f1)/*s is divergent_to+infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC2:def 5;
end;

theorem
  f1 is_right_convergent_in x0 & f2 is_divergent_to-infty_in lim_right(
f1,x0 ) & (for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1)) & (ex g st 0<g &
for r st r in dom f1 /\ ].x0,x0+g.[ holds f1.r<>lim_right(f1,x0)) implies f2*f1
  is_right_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_divergent_to-infty_in lim_right(f1,x0) and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0,x0+g.[ holds f1.r<>lim_right(f1,x0);
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)/\right_open_halfline(x0);
    consider k be Nat such that
A8: for n be Nat st k<=n holds s.n<x0+g by A4,A6,Lm1,LIMFUNC2:2;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th1;
    rng(f1/*s)c=dom f2 by A7,Th1;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1/\right_open_halfline(x0) by A7,Th1;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC2:def 8;
A13: rng s c=dom f1 by A7,Th1;
A14: rng s c=right_open_halfline(x0) by A7,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A15:  q.n=x by FUNCT_2:113;
A16:   n+k in NAT by ORDINAL1:def 12;
A17:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108,A16
        .=x by A15,NAT_1:def 3;
A18:  s.(n+k)<x0+g by A8,NAT_1:12;
A19:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in right_open_halfline(x0) by A14;
      then s.(n+k) in {g1: x0<g1} by XXREAL_1:230;
      then ex g1 st g1=s.(n+k) & x0<g1;
      then s.(n+k) in {g2: x0<g2 & g2<x0+g} by A18;
      then s.(n+k) in ].x0,x0+g.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0,x0+g.[ by A13,A19,XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim_right(f1,x0) by A5;
      then
A20:  not f1.(s.(n+k)) in {lim_right(f1,x0)} by TARSKI:def 1;
      f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11;
      hence x in dom f2\{lim_right(f1,x0)} by A20,A17,XBOOLE_0:def 5;
    end;
    then
A21: rng q c=dom f2\{lim_right(f1,x0)};
    lim(f1/*s)=lim_right(f1,x0) by A1,A6,A11,LIMFUNC2:def 8;
    then lim q=lim_right(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to-infty by A2,A12,A21,LIMFUNC3:def 3;
    hence (f2*f1)/*s is divergent_to-infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC2:def 6;
end;

theorem
  f1 is convergent_in+infty & f2 is_divergent_to+infty_in lim_in+infty
  f1 & (for r ex g st r<g & g in dom(f2*f1)) & (ex r st for g st g in dom f1 /\
  right_open_halfline(r) holds f1.g<>lim_in+infty f1) implies f2*f1 is
  divergent_in+infty_to+infty
proof
  assume that
A1: f1 is convergent_in+infty and
A2: f2 is_divergent_to+infty_in lim_in+infty f1 and
A3: for r ex g st r<g & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\right_open_halfline(r) holds f1.g<> lim_in+infty f1;
  now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to+infty and
A6: rng s c=dom(f2*f1);
    consider k be Nat such that
A7: for n be Nat st k<=n holds r<s.n by A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    set q=s^\k;
A9: q is divergent_to+infty by A5,LIMFUNC1:26;
A10: rng s c=dom f1 by A6,Lm2;
A11: rng q c=rng s by VALUED_0:21;
A12: rng(f1/*q)c=dom f2\{lim_in+infty f1}
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A13:  (f1/*q).n=x by FUNCT_2:113;
A14:  x=f1.(q.n) by A10,A11,A13,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      r<s.(n+k) by A7,NAT_1:12;
      then s.(n+k) in {r2: r<r2};
      then
A15:  s.(n+k) in right_open_halfline(r) by XXREAL_1:230;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\right_open_halfline(r) by A10,A15,XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim_in+infty f1 by A4;
      then
A16:  not f1.(s.(n+k)) in {lim_in+infty f1} by TARSKI:def 1;
A17:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A8;
      then x in dom f2 by A10,A14,FUNCT_2:108,A17;
      hence thesis by A14,A16,XBOOLE_0:def 5;
    end;
    rng q c=dom f1 by A10,A11;
    then f1/*q is convergent & lim(f1/*q)=lim_in+infty f1 by A1,A9,
LIMFUNC1:def 12;
    then
A18: f2/*(f1/*q) is divergent_to+infty by A2,A12,LIMFUNC3:def 2;
    f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A8,VALUED_0:27
      .=((f2*f1)/*s)^\k by A6,VALUED_0:31;
    hence (f2*f1)/*s is divergent_to+infty by A18,LIMFUNC1:7;
  end;
  hence thesis by A3;
end;

theorem
  f1 is convergent_in+infty & f2 is_divergent_to-infty_in lim_in+infty
  f1 & (for r ex g st r<g & g in dom(f2*f1)) & (ex r st for g st g in dom f1 /\
  right_open_halfline(r) holds f1.g<>lim_in+infty f1) implies f2*f1 is
  divergent_in+infty_to-infty
proof
  assume that
A1: f1 is convergent_in+infty and
A2: f2 is_divergent_to-infty_in lim_in+infty f1 and
A3: for r ex g st r<g & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\right_open_halfline(r) holds f1.g<> lim_in+infty f1;
  now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to+infty and
A6: rng s c=dom(f2*f1);
    consider k being Nat such that
A7: for n being Nat st k<=n holds r<s.n by A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    set q=s^\k;
A9: q is divergent_to+infty by A5,LIMFUNC1:26;
A10: rng s c=dom f1 by A6,Lm2;
A11: rng q c=rng s by VALUED_0:21;
A12: rng(f1/*q)c=dom f2\{lim_in+infty f1}
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A13:  (f1/*q).n=x by FUNCT_2:113;
A14:  x=f1.(q.n) by A10,A11,A13,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      r<s.(n+k) by A7,NAT_1:12;
      then s.(n+k) in {r2: r<r2};
      then
A15:  s.(n+k) in right_open_halfline(r) by XXREAL_1:230;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\right_open_halfline(r) by A10,A15,XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim_in+infty f1 by A4;
      then
A16:  not f1.(s.(n+k)) in {lim_in+infty f1} by TARSKI:def 1;
A17:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A8;
      then x in dom f2 by A10,A14,FUNCT_2:108,A17;
      hence thesis by A14,A16,XBOOLE_0:def 5;
    end;
    rng q c=dom f1 by A10,A11;
    then f1/*q is convergent & lim(f1/*q)=lim_in+infty f1 by A1,A9,
LIMFUNC1:def 12;
    then
A18: f2/*(f1/*q) is divergent_to-infty by A2,A12,LIMFUNC3:def 3;
    f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A8,VALUED_0:27
      .=((f2*f1)/*s)^\k by A6,VALUED_0:31;
    hence (f2*f1)/*s is divergent_to-infty by A18,LIMFUNC1:7;
  end;
  hence thesis by A3;
end;

theorem
  f1 is convergent_in-infty & f2 is_divergent_to+infty_in lim_in-infty
  f1 & (for r ex g st g<r & g in dom(f2*f1)) & (ex r st for g st g in dom f1 /\
  left_open_halfline(r) holds f1.g<>lim_in-infty f1) implies f2*f1 is
  divergent_in-infty_to+infty
proof
  assume that
A1: f1 is convergent_in-infty and
A2: f2 is_divergent_to+infty_in lim_in-infty f1 and
A3: for r ex g st g<r & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\left_open_halfline(r) holds f1.g<>lim_in-infty f1;
  now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to-infty and
A6: rng s c=dom(f2*f1);
    consider k being Nat such that
A7: for n being Nat st k<=n holds s.n<r by A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    set q=s^\k;
A9: q is divergent_to-infty by A5,LIMFUNC1:27;
A10: rng s c=dom f1 by A6,Lm2;
A11: rng q c=rng s by VALUED_0:21;
A12: rng(f1/*q)c=dom f2\{lim_in-infty f1}
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A13:  (f1/*q).n=x by FUNCT_2:113;
A14:  x=f1.(q.n) by A10,A11,A13,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      s.(n+k)<r by A7,NAT_1:12;
      then s.(n+k) in {r2: r2<r};
      then
A15:  s.(n+k) in left_open_halfline(r) by XXREAL_1:229;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\left_open_halfline(r) by A10,A15,XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim_in-infty f1 by A4;
      then
A16:  not f1.(s.(n+k)) in {lim_in-infty f1} by TARSKI:def 1;
A17:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A8;
      then x in dom f2 by A10,A14,FUNCT_2:108,A17;
      hence thesis by A14,A16,XBOOLE_0:def 5;
    end;
    rng q c=dom f1 by A10,A11;
    then f1/*q is convergent & lim(f1/*q)=lim_in-infty f1 by A1,A9,
LIMFUNC1:def 13;
    then
A18: f2/*(f1/*q) is divergent_to+infty by A2,A12,LIMFUNC3:def 2;
    f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A8,VALUED_0:27
      .=((f2*f1)/*s)^\k by A6,VALUED_0:31;
    hence (f2*f1)/*s is divergent_to+infty by A18,LIMFUNC1:7;
  end;
  hence thesis by A3;
end;

theorem
  f1 is convergent_in-infty & f2 is_divergent_to-infty_in lim_in-infty
  f1 & (for r ex g st g<r & g in dom(f2*f1)) & (ex r st for g st g in dom f1 /\
  left_open_halfline(r) holds f1.g<>lim_in-infty f1) implies f2*f1 is
  divergent_in-infty_to-infty
proof
  assume that
A1: f1 is convergent_in-infty and
A2: f2 is_divergent_to-infty_in lim_in-infty f1 and
A3: for r ex g st g<r & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\left_open_halfline(r) holds f1.g<>lim_in-infty f1;
  now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to-infty and
A6: rng s c=dom(f2*f1);
    consider k being Nat such that
A7: for n being Nat st k<=n holds s.n<r by A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    set q=s^\k;
A9: q is divergent_to-infty by A5,LIMFUNC1:27;
A10: rng s c=dom f1 by A6,Lm2;
A11: rng q c=rng s by VALUED_0:21;
A12: rng(f1/*q)c=dom f2\{lim_in-infty f1}
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A13:  (f1/*q).n=x by FUNCT_2:113;
A14:  x=f1.(q.n) by A10,A11,A13,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      s.(n+k)<r by A7,NAT_1:12;
      then s.(n+k) in {r2: r2<r};
      then
A15:  s.(n+k) in left_open_halfline(r) by XXREAL_1:229;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\left_open_halfline(r) by A10,A15,XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim_in-infty f1 by A4;
      then
A16:  not f1.(s.(n+k)) in {lim_in-infty f1} by TARSKI:def 1;
A17:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A8;
      then x in dom f2 by A10,A14,FUNCT_2:108,A17;
      hence thesis by A14,A16,XBOOLE_0:def 5;
    end;
    rng q c=dom f1 by A10,A11;
    then f1/*q is convergent & lim(f1/*q)=lim_in-infty f1 by A1,A9,
LIMFUNC1:def 13;
    then
A18: f2/*(f1/*q) is divergent_to-infty by A2,A12,LIMFUNC3:def 3;
    f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A8,VALUED_0:27
      .=((f2*f1)/*s)^\k by A6,VALUED_0:31;
    hence (f2*f1)/*s is divergent_to-infty by A18,LIMFUNC1:7;
  end;
  hence thesis by A3;
end;

theorem
  f1 is_convergent_in x0 & f2 is_left_divergent_to+infty_in lim(f1,x0) &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2<
r2 & x0<g2 & g2 in dom(f2*f1)) & (ex g st 0<g & for r st r in dom f1 /\ (].x0-g
  ,x0.[ \/ ].x0,x0+g.[) holds f1.r<lim(f1,x0)) implies f2*f1
  is_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_left_divergent_to+infty_in lim(f1,x0) and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) holds lim(f1,x0)>f1 .r;
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)\{x0};
    consider k being Element of NAT such that
A8: for n being Element of NAT st k<=n holds x0-g<s.n & s.n<x0+g by A4,A6,
LIMFUNC3:7;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th2;
    rng(f1/*s)c=dom f2 by A7,Th2;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1\{x0} by A7,Th2;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC3:def 4;
A13: rng s c=dom f1 by A7,Th2;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A14:  q.n=x by FUNCT_2:113;
A15:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108
        .=x by A14,NAT_1:def 3;
      k<=n+k by NAT_1:12;
      then x0-g<s.(n+k) & s.(n+k)<x0+g by A8;
      then s.(n+k) in {g1: x0-g<g1 & g1<x0+g};
      then
A16:  s.(n+k) in ].x0-g,x0+g.[ by RCOMP_1:def 2;
A17:  s.(n+k) in rng s by VALUED_0:28;
      then not s.(n+k) in {x0} by A7,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0+g.[\{x0} by A16,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0.[\/].x0,x0+g.[ by A4,LIMFUNC3:4;
      then s.(n+k) in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) by A13,A17,
XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim(f1,x0) by A5;
      then f1.(s.(n+k)) in {g2: g2<lim(f1,x0)};
      then
A18:  f1.(s.(n+k)) in left_open_halfline(lim(f1,x0)) by XXREAL_1:229;
      f1.(s.(n+k)) in dom f2 by A9,A17,FUNCT_1:11;
      hence x in dom f2/\left_open_halfline(lim(f1,x0)) by A18,A15,
XBOOLE_0:def 4;
    end;
    then
A19: rng q c=dom f2/\ left_open_halfline(lim(f1,x0));
    lim(f1/*s)=lim(f1,x0) by A1,A6,A11,LIMFUNC3:def 4;
    then lim q=lim(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to+infty by A2,A12,A19,LIMFUNC2:def 2;
    hence (f2*f1)/*s is divergent_to+infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC3:def 2;
end;

theorem
  f1 is_convergent_in x0 & f2 is_left_divergent_to-infty_in lim(f1,x0) &
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2<
r2 & x0<g2 & g2 in dom(f2*f1)) & (ex g st 0<g & for r st r in dom f1 /\ (].x0-g
  ,x0.[ \/ ].x0,x0+g.[) holds f1.r<lim(f1,x0)) implies f2*f1
  is_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_left_divergent_to-infty_in lim(f1,x0) and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) holds lim(f1,x0)>f1 .r;
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)\{x0};
    consider k being Element of NAT such that
A8: for n being Element of NAT st k<=n holds x0-g<s.n & s.n<x0+g by A4,A6,
LIMFUNC3:7;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th2;
    rng(f1/*s)c=dom f2 by A7,Th2;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1\{x0} by A7,Th2;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC3:def 4;
A13: rng s c=dom f1 by A7,Th2;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A14:  q.n=x by FUNCT_2:113;
A15:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108
        .=x by A14,NAT_1:def 3;
      k<=n+k by NAT_1:12;
      then x0-g<s.(n+k) & s.(n+k)<x0+g by A8;
      then s.(n+k) in {g1: x0-g<g1 & g1<x0+g};
      then
A16:  s.(n+k) in ].x0-g,x0+g.[ by RCOMP_1:def 2;
A17:  s.(n+k) in rng s by VALUED_0:28;
      then not s.(n+k) in {x0} by A7,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0+g.[\{x0} by A16,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0.[\/].x0,x0+g.[ by A4,LIMFUNC3:4;
      then s.(n+k) in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) by A13,A17,
XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim(f1,x0) by A5;
      then f1.(s.(n+k)) in {g2: g2<lim(f1,x0)};
      then
A18:  f1.(s.(n+k)) in left_open_halfline(lim(f1,x0)) by XXREAL_1:229;
      f1.(s.(n+k)) in dom f2 by A9,A17,FUNCT_1:11;
      hence x in dom f2/\left_open_halfline(lim(f1,x0)) by A18,A15,
XBOOLE_0:def 4;
    end;
    then
A19: rng q c=dom f2/\left_open_halfline(lim(f1,x0));
    lim(f1/*s)=lim(f1,x0) by A1,A6,A11,LIMFUNC3:def 4;
    then lim q=lim(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to-infty by A2,A12,A19,LIMFUNC2:def 3;
    hence (f2*f1)/*s is divergent_to-infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC3:def 3;
end;

theorem
  f1 is_left_convergent_in x0 & f2 is_divergent_to+infty_in lim_left(f1,
x0) & (for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1)) & (ex g st 0<g & for
  r st r in dom f1 /\ ].x0-g,x0.[ holds f1.r<>lim_left(f1,x0)) implies f2*f1
  is_left_divergent_to+infty_in x0
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_divergent_to+infty_in lim_left(f1,x0) and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0-g,x0.[ holds f1.r<>lim_left(f1,x0);
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)/\left_open_halfline(x0);
    consider k being Nat such that
A8: for n being Nat st k<=n holds x0-g<s.n by A4,A6,Lm1,LIMFUNC2:1;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th1;
    rng(f1/*s)c=dom f2 by A7,Th1;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1/\left_open_halfline(x0) by A7,Th1;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC2:def 7;
A13: rng s c=dom f1 by A7,Th1;
A14: rng s c=left_open_halfline(x0) by A7,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A15:  q.n=x by FUNCT_2:113;
A16:   n+k in NAT by ORDINAL1:def 12;
A17:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108,A16
        .=x by A15,NAT_1:def 3;
A18:  x0-g<s.(n+k) by A8,NAT_1:12;
A19:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in left_open_halfline(x0) by A14;
      then s.(n+k) in {g1: g1<x0} by XXREAL_1:229;
      then ex g1 st g1=s.(n+k) & g1<x0;
      then s.(n+k) in {g2: x0-g<g2 & g2<x0} by A18;
      then s.(n+k) in ].x0-g,x0.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0-g,x0.[ by A13,A19,XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim_left(f1,x0) by A5;
      then
A20:  not f1.(s.(n+k)) in {lim_left(f1,x0)} by TARSKI:def 1;
      f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11;
      hence x in dom f2\{lim_left(f1,x0)} by A20,A17,XBOOLE_0:def 5;
    end;
    then
A21: rng q c=dom f2\{lim_left(f1,x0)};
    lim(f1/*s)=lim_left(f1,x0) by A1,A6,A11,LIMFUNC2:def 7;
    then lim q=lim_left(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to+infty by A2,A12,A21,LIMFUNC3:def 2;
    hence (f2*f1)/*s is divergent_to+infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC2:def 2;
end;

theorem
  f1 is_left_convergent_in x0 & f2 is_divergent_to-infty_in lim_left(f1,
x0) & (for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1)) & (ex g st 0<g & for
  r st r in dom f1 /\ ].x0-g,x0.[ holds f1.r<>lim_left(f1,x0)) implies f2*f1
  is_left_divergent_to-infty_in x0
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_divergent_to-infty_in lim_left(f1,x0) and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0-g,x0.[ holds f1.r<>lim_left(f1,x0);
  now
    let s be Real_Sequence;
    assume that
A6: s is convergent & lim s=x0 and
A7: rng s c=dom(f2*f1)/\left_open_halfline(x0);
    consider k being Nat such that
A8: for n being Nat st k<=n holds x0-g<s.n by A4,A6,Lm1,LIMFUNC2:1;
    set q=(f1/*s)^\k;
A9: rng s c=dom(f2*f1) by A7,Th1;
    rng(f1/*s)c=dom f2 by A7,Th1;
    then
A10: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A9,VALUED_0:31;
A11: rng s c=dom f1/\left_open_halfline(x0) by A7,Th1;
    then
A12: f1/*s is convergent by A1,A2,A6,LIMFUNC2:def 7;
A13: rng s c=dom f1 by A7,Th1;
A14: rng s c=left_open_halfline(x0) by A7,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A15:  q.n=x by FUNCT_2:113;
A16:   n+k in NAT by ORDINAL1:def 12;
A17:  f1.(s.(n+k))=(f1/*s).(n+k) by A13,FUNCT_2:108,A16
        .=x by A15,NAT_1:def 3;
A18:  x0-g<s.(n+k) by A8,NAT_1:12;
A19:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in left_open_halfline(x0) by A14;
      then s.(n+k) in {g1: g1<x0} by XXREAL_1:229;
      then ex g1 st g1=s.(n+k) & g1<x0;
      then s.(n+k) in {g2: x0-g<g2 & g2<x0} by A18;
      then s.(n+k) in ].x0-g,x0.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0-g,x0.[ by A13,A19,XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim_left(f1,x0) by A5;
      then
A20:  not f1.(s.(n+k)) in {lim_left(f1,x0)} by TARSKI:def 1;
      f1.(s.(n+k)) in dom f2 by A9,A19,FUNCT_1:11;
      hence x in dom f2\{lim_left(f1,x0)} by A20,A17,XBOOLE_0:def 5;
    end;
    then
A21: rng q c=dom f2\{lim_left(f1,x0)};
    lim(f1/*s)=lim_left(f1,x0) by A1,A6,A11,LIMFUNC2:def 7;
    then lim q=lim_left(f1,x0) by A12,SEQ_4:20;
    then f2/*q is divergent_to-infty by A2,A12,A21,LIMFUNC3:def 3;
    hence (f2*f1)/*s is divergent_to-infty by A10,LIMFUNC1:7;
  end;
  hence thesis by A3,LIMFUNC2:def 3;
end;

theorem
  f1 is divergent_in+infty_to+infty & f2 is convergent_in+infty & (for r
  ex g st r<g & g in dom(f2*f1)) implies f2*f1 is convergent_in+infty &
  lim_in+infty(f2*f1)=lim_in+infty f2
proof
  assume that
A1: f1 is divergent_in+infty_to+infty and
A2: f2 is convergent_in+infty and
A3: for r ex g st r<g & g in dom(f2*f1);
A4: now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to+infty and
A6: rng s c=dom(f2*f1);
    rng s c=dom f1 by A6,Lm2;
    then
A7: f1/*s is divergent_to+infty by A1,A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    then
A9: lim(f2/*(f1/*s))=lim_in+infty f2 by A2,A7,LIMFUNC1:def 12;
    f2/*(f1/*s) is convergent by A2,A8,A7;
    hence (f2*f1)/*s is convergent & lim((f2*f1)/*s)=lim_in+infty f2 by A6,A9,
VALUED_0:31;
  end;
  hence f2*f1 is convergent_in+infty by A3;
  hence thesis by A4,LIMFUNC1:def 12;
end;

theorem
  f1 is divergent_in+infty_to-infty & f2 is convergent_in-infty & (for r
  ex g st r<g & g in dom(f2*f1)) implies f2*f1 is convergent_in+infty &
  lim_in+infty(f2*f1)=lim_in-infty f2
proof
  assume that
A1: f1 is divergent_in+infty_to-infty and
A2: f2 is convergent_in-infty and
A3: for r ex g st r<g & g in dom(f2*f1);
A4: now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to+infty and
A6: rng s c=dom(f2*f1);
    rng s c=dom f1 by A6,Lm2;
    then
A7: f1/*s is divergent_to-infty by A1,A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    then
A9: lim(f2/*(f1/*s))=lim_in-infty f2 by A2,A7,LIMFUNC1:def 13;
    f2/*(f1/*s) is convergent by A2,A8,A7;
    hence (f2*f1)/*s is convergent & lim((f2*f1)/*s)=lim_in-infty f2 by A6,A9,
VALUED_0:31;
  end;
  hence f2*f1 is convergent_in+infty by A3;
  hence thesis by A4,LIMFUNC1:def 12;
end;

theorem
  f1 is divergent_in-infty_to+infty & f2 is convergent_in+infty & (for r
  ex g st g<r & g in dom(f2*f1)) implies f2*f1 is convergent_in-infty &
  lim_in-infty(f2*f1)=lim_in+infty f2
proof
  assume that
A1: f1 is divergent_in-infty_to+infty and
A2: f2 is convergent_in+infty and
A3: for r ex g st g<r & g in dom(f2*f1);
A4: now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to-infty and
A6: rng s c=dom(f2*f1);
    rng s c=dom f1 by A6,Lm2;
    then
A7: f1/*s is divergent_to+infty by A1,A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    then
A9: lim(f2/*(f1/*s))=lim_in+infty f2 by A2,A7,LIMFUNC1:def 12;
    f2/*(f1/*s) is convergent by A2,A8,A7;
    hence (f2*f1)/*s is convergent & lim((f2*f1)/*s)=lim_in+infty f2 by A6,A9,
VALUED_0:31;
  end;
  hence f2*f1 is convergent_in-infty by A3;
  hence thesis by A4,LIMFUNC1:def 13;
end;

theorem
  f1 is divergent_in-infty_to-infty & f2 is convergent_in-infty & (for r
  ex g st g<r & g in dom(f2*f1)) implies f2*f1 is convergent_in-infty &
  lim_in-infty(f2*f1)=lim_in-infty f2
proof
  assume that
A1: f1 is divergent_in-infty_to-infty and
A2: f2 is convergent_in-infty and
A3: for r ex g st g<r & g in dom(f2*f1);
A4: now
    let s be Real_Sequence;
    assume that
A5: s is divergent_to-infty and
A6: rng s c=dom(f2*f1);
    rng s c=dom f1 by A6,Lm2;
    then
A7: f1/*s is divergent_to-infty by A1,A5;
A8: rng(f1/*s)c=dom f2 by A6,Lm2;
    then
A9: lim(f2/*(f1/*s))=lim_in-infty f2 by A2,A7,LIMFUNC1:def 13;
    f2/*(f1/*s) is convergent by A2,A8,A7;
    hence (f2*f1)/*s is convergent & lim((f2*f1)/*s)=lim_in-infty f2 by A6,A9,
VALUED_0:31;
  end;
  hence f2*f1 is convergent_in-infty by A3;
  hence thesis by A4,LIMFUNC1:def 13;
end;

theorem
  f1 is_left_divergent_to+infty_in x0 & f2 is convergent_in+infty & (for
  r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1)) implies f2*f1
  is_left_convergent_in x0 & lim_left(f2*f1,x0)=lim_in+infty f2
proof
  assume that
A1: f1 is_left_divergent_to+infty_in x0 and
A2: f2 is convergent_in+infty and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
A4: now
    let s be Real_Sequence;
    assume that
A5: s is convergent & lim s=x0 and
A6: rng s c=dom(f2*f1)/\left_open_halfline(x0);
    rng s c=dom f1/\left_open_halfline(x0) by A6,Th1;
    then
A7: f1/*s is divergent_to+infty by A1,A5,LIMFUNC2:def 2;
A8: rng(f1/*s)c=dom f2 by A6,Th1;
    then
A9: lim(f2/*(f1/*s))=lim_in+infty f2 by A2,A7,LIMFUNC1:def 12;
A10: rng s c=dom(f2*f1) by A6,Th1;
    f2/*(f1/*s) is convergent by A2,A8,A7;
    hence (f2*f1)/*s is convergent & lim((f2*f1)/*s)=lim_in+infty f2 by A10,A9,
VALUED_0:31;
  end;
  hence f2*f1 is_left_convergent_in x0 by A3,LIMFUNC2:def 1;
  hence thesis by A4,LIMFUNC2:def 7;
end;

theorem
  f1 is_left_divergent_to-infty_in x0 & f2 is convergent_in-infty & (for
  r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1)) implies f2*f1
  is_left_convergent_in x0 & lim_left(f2*f1,x0)=lim_in-infty f2
proof
  assume that
A1: f1 is_left_divergent_to-infty_in x0 and
A2: f2 is convergent_in-infty and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
A4: now
    let s be Real_Sequence;
    assume that
A5: s is convergent & lim s=x0 and
A6: rng s c=dom(f2*f1)/\left_open_halfline(x0);
    rng s c=dom f1/\left_open_halfline(x0) by A6,Th1;
    then
A7: f1/*s is divergent_to-infty by A1,A5,LIMFUNC2:def 3;
A8: rng(f1/*s)c=dom f2 by A6,Th1;
    then
A9: lim(f2/*(f1/*s))=lim_in-infty f2 by A2,A7,LIMFUNC1:def 13;
A10: rng s c=dom(f2*f1) by A6,Th1;
    f2/*(f1/*s) is convergent by A2,A8,A7;
    hence (f2*f1)/*s is convergent & lim((f2*f1)/*s)=lim_in-infty f2 by A10,A9,
VALUED_0:31;
  end;
  hence f2*f1 is_left_convergent_in x0 by A3,LIMFUNC2:def 1;
  hence thesis by A4,LIMFUNC2:def 7;
end;

theorem
  f1 is_right_divergent_to+infty_in x0 & f2 is convergent_in+infty & (
  for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1)) implies f2*f1
  is_right_convergent_in x0 & lim_right(f2*f1,x0)=lim_in+infty f2
proof
  assume that
A1: f1 is_right_divergent_to+infty_in x0 and
A2: f2 is convergent_in+infty and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
A4: now
    let s be Real_Sequence;
    assume that
A5: s is convergent & lim s=x0 and
A6: rng s c=dom(f2*f1)/\right_open_halfline(x0);
    rng s c=dom f1/\right_open_halfline(x0) by A6,Th1;
    then
A7: f1/*s is divergent_to+infty by A1,A5,LIMFUNC2:def 5;
A8: rng(f1/*s)c=dom f2 by A6,Th1;
    then
A9: lim(f2/*(f1/*s))=lim_in+infty f2 by A2,A7,LIMFUNC1:def 12;
A10: rng s c=dom(f2*f1) by A6,Th1;
    f2/*(f1/*s) is convergent by A2,A8,A7;
    hence (f2*f1)/*s is convergent & lim((f2*f1)/*s)=lim_in+infty f2 by A10,A9,
VALUED_0:31;
  end;
  hence f2*f1 is_right_convergent_in x0 by A3,LIMFUNC2:def 4;
  hence thesis by A4,LIMFUNC2:def 8;
end;

theorem
  f1 is_right_divergent_to-infty_in x0 & f2 is convergent_in-infty & (
  for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1)) implies f2*f1
  is_right_convergent_in x0 & lim_right(f2*f1,x0)=lim_in-infty f2
proof
  assume that
A1: f1 is_right_divergent_to-infty_in x0 and
A2: f2 is convergent_in-infty and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
A4: now
    let s be Real_Sequence;
    assume that
A5: s is convergent & lim s=x0 and
A6: rng s c=dom(f2*f1)/\right_open_halfline(x0);
    rng s c=dom f1/\right_open_halfline(x0) by A6,Th1;
    then
A7: f1/*s is divergent_to-infty by A1,A5,LIMFUNC2:def 6;
A8: rng(f1/*s)c=dom f2 by A6,Th1;
    then
A9: lim(f2/*(f1/*s))=lim_in-infty f2 by A2,A7,LIMFUNC1:def 13;
A10: rng s c=dom(f2*f1) by A6,Th1;
    f2/*(f1/*s) is convergent by A2,A8,A7;
    hence (f2*f1)/*s is convergent & lim((f2*f1)/*s)=lim_in-infty f2 by A10,A9,
VALUED_0:31;
  end;
  hence f2*f1 is_right_convergent_in x0 by A3,LIMFUNC2:def 4;
  hence thesis by A4,LIMFUNC2:def 8;
end;

theorem
  f1 is_left_convergent_in x0 & f2 is_left_convergent_in lim_left(f1,x0)
  & (for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1)) & (ex g st 0<g & for r
  st r in dom f1 /\ ].x0-g,x0.[ holds f1.r<lim_left(f1,x0)) implies f2*f1
  is_left_convergent_in x0 & lim_left(f2*f1,x0)=lim_left(f2,lim_left(f1,x0))
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_left_convergent_in lim_left(f1,x0) and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0-g,x0.[ holds f1.r<lim_left(f1,x0);
A6: now
    let s be Real_Sequence;
    assume that
A7: s is convergent & lim s=x0 and
A8: rng s c=dom(f2*f1)/\left_open_halfline(x0);
    consider k being Nat such that
A9: for n being Nat st k<=n holds x0-g<s.n by A4,A7,Lm1,LIMFUNC2:1;
A10: rng s c=dom f1 by A8,Th1;
    set q=(f1/*s)^\k;
A11: rng s c=dom(f2*f1) by A8,Th1;
A12: rng s c=left_open_halfline(x0) by A8,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A13:  q.n=x by FUNCT_2:113;
A14:   n+k in NAT by ORDINAL1:def 12;
A15:  f1.(s.(n+k))=(f1/*s).(n+k) by A10,FUNCT_2:108,A14
        .=x by A13,NAT_1:def 3;
A16:  x0-g<s.(n+k) by A9,NAT_1:12;
A17:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in left_open_halfline(x0) by A12;
      then s.(n+k) in {g1: g1<x0} by XXREAL_1:229;
      then ex g1 st g1=s.(n+k) & g1<x0;
      then s.(n+k) in {g2: x0-g<g2 & g2<x0} by A16;
      then s.(n+k) in ].x0-g,x0.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0-g,x0.[ by A10,A17,XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim_left(f1,x0) by A5;
      then f1.(s.(n+k)) in {r1 : r1<lim_left(f1,x0)};
      then
A18:  f1.(s.(n+k)) in left_open_halfline(lim_left(f1,x0)) by XXREAL_1:229;
      f1.(s.(n+k)) in dom f2 by A11,A17,FUNCT_1:11;
      hence x in dom f2/\left_open_halfline(lim_left(f1,x0)) by A18,A15,
XBOOLE_0:def 4;
    end;
    then
A19: rng q c=dom f2/\left_open_halfline(lim_left(f1,x0));
    rng(f1/*s)c=dom f2 by A8,Th1;
    then
A20: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A11,VALUED_0:31;
A21: rng s c=dom f1/\left_open_halfline(x0) by A8,Th1;
    then
A22: f1/*s is convergent by A1,A2,A7,LIMFUNC2:def 7;
    lim(f1/*s)=lim_left(f1,x0) by A1,A7,A21,LIMFUNC2:def 7;
    then
A23: lim q=lim_left(f1,x0) by A22,SEQ_4:20;
    lim_left(f2,lim_left(f1,x0))=lim_left(f2,lim_left(f1,x0));
    then
A24: f2/*q is convergent by A2,A22,A23,A19,LIMFUNC2:def 7;
    hence (f2*f1)/*s is convergent by A20,SEQ_4:21;
    lim(f2/*q)=lim_left(f2,lim_left(f1,x0)) by A2,A22,A23,A19,LIMFUNC2:def 7;
    hence lim((f2*f1)/*s)=lim_left(f2,lim_left(f1,x0)) by A24,A20,SEQ_4:22;
  end;
  hence f2*f1 is_left_convergent_in x0 by A3,LIMFUNC2:def 1;
  hence thesis by A6,LIMFUNC2:def 7;
end;

theorem
  f1 is_right_convergent_in x0 & f2 is_right_convergent_in lim_right(f1,
x0) & (for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1)) & (ex g st 0<g & for
  r st r in dom f1 /\ ].x0,x0+g.[ holds lim_right(f1,x0)<f1.r) implies f2*f1
is_right_convergent_in x0 & lim_right(f2*f1,x0)=lim_right(f2,lim_right(f1,x0))
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_right_convergent_in lim_right(f1,x0) and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0,x0+g.[ holds lim_right(f1,x0)<f1.r;
A6: now
    let s be Real_Sequence;
    assume that
A7: s is convergent & lim s=x0 and
A8: rng s c=dom(f2*f1)/\right_open_halfline(x0);
    consider k being Nat such that
A9: for n being Nat st k<=n holds s.n<x0+g by A4,A7,Lm1,LIMFUNC2:2;
A10: rng s c=dom f1 by A8,Th1;
    set q=(f1/*s)^\k;
A11: rng s c=dom(f2*f1) by A8,Th1;
A12: rng s c=right_open_halfline(x0) by A8,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A13:  q.n=x by FUNCT_2:113;
A14:   n+k in NAT by ORDINAL1:def 12;
A15:  f1.(s.(n+k))=(f1/*s).(n+k) by A10,FUNCT_2:108,A14
        .=x by A13,NAT_1:def 3;
A16:  s.(n+k)<x0+g by A9,NAT_1:12;
A17:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in right_open_halfline(x0) by A12;
      then s.(n+k) in {g1: x0<g1} by XXREAL_1:230;
      then ex g1 st g1=s.(n+k) & x0<g1;
      then s.(n+k) in {g2: x0<g2 & g2<x0+g} by A16;
      then s.(n+k) in ].x0,x0+g.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0,x0+g.[ by A10,A17,XBOOLE_0:def 4;
      then lim_right(f1,x0)<f1.(s.(n+k)) by A5;
      then f1.(s.(n+k)) in {r1: lim_right(f1,x0)<r1};
      then
A18:  f1.(s.(n+k)) in right_open_halfline(lim_right(f1,x0)) by XXREAL_1:230;
      f1.(s.(n+k)) in dom f2 by A11,A17,FUNCT_1:11;
      hence x in dom f2/\right_open_halfline(lim_right(f1,x0)) by A18,A15,
XBOOLE_0:def 4;
    end;
    then
A19: rng q c=dom f2/\ right_open_halfline(lim_right(f1,x0));
    rng(f1/*s)c=dom f2 by A8,Th1;
    then
A20: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A11,VALUED_0:31;
A21: rng s c=dom f1/\right_open_halfline(x0) by A8,Th1;
    then
A22: f1/*s is convergent by A1,A2,A7,LIMFUNC2:def 8;
    lim(f1/*s)=lim_right(f1,x0) by A1,A7,A21,LIMFUNC2:def 8;
    then
A23: lim q=lim_right(f1,x0) by A22,SEQ_4:20;
    lim_right(f2,lim_right(f1,x0))=lim_right(f2,lim_right(f1,x0));
    then
A24: f2/*q is convergent by A2,A22,A23,A19,LIMFUNC2:def 8;
    hence (f2*f1)/*s is convergent by A20,SEQ_4:21;
    lim(f2/*q)=lim_right(f2,lim_right(f1,x0)) by A2,A22,A23,A19,LIMFUNC2:def 8;
    hence lim((f2*f1)/*s)=lim_right(f2,lim_right(f1,x0)) by A24,A20,SEQ_4:22;
  end;
  hence f2*f1 is_right_convergent_in x0 by A3,LIMFUNC2:def 4;
  hence thesis by A6,LIMFUNC2:def 8;
end;

theorem
  f1 is_left_convergent_in x0 & f2 is_right_convergent_in lim_left(f1,x0
) & (for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1)) & (ex g st 0<g & for r
  st r in dom f1 /\ ].x0-g,x0.[ holds lim_left(f1,x0)<f1.r) implies f2*f1
  is_left_convergent_in x0 & lim_left(f2*f1,x0)=lim_right(f2,lim_left(f1,x0))
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_right_convergent_in lim_left(f1,x0) and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0-g,x0.[ holds lim_left(f1,x0)<f1.r;
A6: now
    let s be Real_Sequence;
    assume that
A7: s is convergent & lim s=x0 and
A8: rng s c=dom(f2*f1)/\left_open_halfline(x0);
    consider k being Nat such that
A9: for n being Nat st k<=n holds x0-g<s.n by A4,A7,Lm1,LIMFUNC2:1;
A10: rng s c=dom f1 by A8,Th1;
    set q=(f1/*s)^\k;
A11: rng s c=dom(f2*f1) by A8,Th1;
A12: rng s c=left_open_halfline(x0) by A8,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A13:  q.n=x by FUNCT_2:113;
A14:   n+k in NAT by ORDINAL1:def 12;
A15:  f1.(s.(n+k))=(f1/*s).(n+k) by A10,FUNCT_2:108,A14
        .=x by A13,NAT_1:def 3;
A16:  x0-g<s.(n+k) by A9,NAT_1:12;
A17:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in left_open_halfline(x0) by A12;
      then s.(n+k) in {g1 : g1<x0} by XXREAL_1:229;
      then ex g1 st g1=s.(n+k) & g1<x0;
      then s.(n+k) in {g2: x0-g<g2 & g2<x0} by A16;
      then s.(n+k) in ].x0-g,x0.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0-g,x0.[ by A10,A17,XBOOLE_0:def 4;
      then lim_left(f1,x0)<f1.(s.(n+k)) by A5;
      then f1.(s.(n+k)) in {r1: lim_left(f1,x0)<r1};
      then
A18:  f1.(s.(n+k)) in right_open_halfline(lim_left(f1,x0)) by XXREAL_1:230;
      f1.(s.(n+k)) in dom f2 by A11,A17,FUNCT_1:11;
      hence x in dom f2/\right_open_halfline(lim_left(f1,x0)) by A18,A15,
XBOOLE_0:def 4;
    end;
    then
A19: rng q c=dom f2/\right_open_halfline(lim_left(f1,x0));
    rng(f1/*s)c=dom f2 by A8,Th1;
    then
A20: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A11,VALUED_0:31;
A21: rng s c=dom f1/\left_open_halfline(x0) by A8,Th1;
    then
A22: f1/*s is convergent by A1,A2,A7,LIMFUNC2:def 7;
    lim(f1/*s)=lim_left(f1,x0) by A1,A7,A21,LIMFUNC2:def 7;
    then
A23: lim q=lim_left(f1,x0) by A22,SEQ_4:20;
    lim_right(f2,lim_left(f1,x0))=lim_right(f2,lim_left(f1,x0));
    then
A24: f2/*q is convergent by A2,A22,A23,A19,LIMFUNC2:def 8;
    hence (f2*f1)/*s is convergent by A20,SEQ_4:21;
    lim(f2/*q)=lim_right(f2,lim_left(f1,x0)) by A2,A22,A23,A19,LIMFUNC2:def 8;
    hence lim((f2*f1)/*s)=lim_right(f2,lim_left(f1,x0)) by A24,A20,SEQ_4:22;
  end;
  hence f2*f1 is_left_convergent_in x0 by A3,LIMFUNC2:def 1;
  hence thesis by A6,LIMFUNC2:def 7;
end;

theorem
  f1 is_right_convergent_in x0 & f2 is_left_convergent_in lim_right(f1,
x0) & (for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1)) & (ex g st 0<g & for
  r st r in dom f1 /\ ].x0,x0+g.[ holds f1.r<lim_right(f1,x0)) implies f2*f1
  is_right_convergent_in x0 & lim_right(f2*f1,x0)=lim_left(f2,lim_right(f1,x0))
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_left_convergent_in lim_right(f1,x0) and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0,x0+g.[ holds f1.r<lim_right(f1,x0);
A6: now
    let s be Real_Sequence;
    assume that
A7: s is convergent & lim s=x0 and
A8: rng s c=dom(f2*f1)/\right_open_halfline(x0);
    consider k being Nat such that
A9: for n being Nat st k<=n holds s.n<x0+g by A4,A7,Lm1,LIMFUNC2:2;
A10: rng s c=dom f1 by A8,Th1;
    set q=(f1/*s)^\k;
A11: rng s c=dom(f2*f1) by A8,Th1;
A12: rng s c=right_open_halfline(x0) by A8,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A13:  q.n=x by FUNCT_2:113;
A14:   n+k in NAT by ORDINAL1:def 12;
A15:  f1.(s.(n+k))=(f1/*s).(n+k) by A10,FUNCT_2:108,A14
        .=x by A13,NAT_1:def 3;
A16:  s.(n+k)<x0+g by A9,NAT_1:12;
A17:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in right_open_halfline(x0) by A12;
      then s.(n+k) in {g1: x0<g1} by XXREAL_1:230;
      then ex g1 st g1=s.(n+k) & x0<g1;
      then s.(n+k) in {g2: x0<g2 & g2<x0+g} by A16;
      then s.(n+k) in ].x0,x0+g.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0,x0+g.[ by A10,A17,XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim_right(f1,x0) by A5;
      then f1.(s.(n+k)) in {r1: r1<lim_right(f1,x0)};
      then
A18:  f1.(s.(n+k)) in left_open_halfline(lim_right(f1,x0)) by XXREAL_1:229;
      f1.(s.(n+k)) in dom f2 by A11,A17,FUNCT_1:11;
      hence x in dom f2/\left_open_halfline(lim_right(f1,x0)) by A18,A15,
XBOOLE_0:def 4;
    end;
    then
A19: rng q c=dom f2/\left_open_halfline(lim_right(f1,x0));
    rng(f1/*s)c=dom f2 by A8,Th1;
    then
A20: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A11,VALUED_0:31;
A21: rng s c=dom f1/\right_open_halfline(x0) by A8,Th1;
    then
A22: f1/*s is convergent by A1,A2,A7,LIMFUNC2:def 8;
    lim(f1/*s)=lim_right(f1,x0) by A1,A7,A21,LIMFUNC2:def 8;
    then
A23: lim q=lim_right(f1,x0) by A22,SEQ_4:20;
    lim_left(f2,lim_right(f1,x0))=lim_left(f2,lim_right(f1,x0));
    then
A24: f2/*q is convergent by A2,A22,A23,A19,LIMFUNC2:def 7;
    hence (f2*f1)/*s is convergent by A20,SEQ_4:21;
    lim(f2/*q)=lim_left(f2,lim_right(f1,x0)) by A2,A22,A23,A19,LIMFUNC2:def 7;
    hence lim((f2*f1)/*s)=lim_left(f2,lim_right(f1,x0)) by A24,A20,SEQ_4:22;
  end;
  hence f2*f1 is_right_convergent_in x0 by A3,LIMFUNC2:def 4;
  hence thesis by A6,LIMFUNC2:def 8;
end;

theorem
  f1 is convergent_in+infty & f2 is_left_convergent_in lim_in+infty f1 &
  (for r ex g st r<g & g in dom(f2*f1)) & (ex r st for g st g in dom f1 /\
  right_open_halfline(r) holds f1.g<lim_in+infty f1) implies f2*f1 is
  convergent_in+infty & lim_in+infty(f2*f1)=lim_left(f2,lim_in+infty f1)
proof
  assume that
A1: f1 is convergent_in+infty and
A2: f2 is_left_convergent_in lim_in+infty f1 and
A3: for r ex g st r<g & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\right_open_halfline(r) holds f1.g<lim_in+infty f1;
A5: now
    set L=lim_left(f2,lim_in+infty f1);
    let s be Real_Sequence;
    assume that
A6: s is divergent_to+infty and
A7: rng s c=dom(f2*f1);
    consider k being Nat such that
A8: for n being Nat st k<=n holds r<s.n by A6;
    set q=s^\k;
A9: q is divergent_to+infty by A6,LIMFUNC1:26;
A10: rng s c=dom f1 by A7,Lm2;
A11: rng q c=rng s by VALUED_0:21;
    then rng q c=dom f1 by A10;
    then
A12: f1/*q is convergent & lim(f1/*q)=lim_in+infty f1 by A1,A9,
LIMFUNC1:def 12;
A13: rng(f1/*s)c=dom f2 by A7,Lm2;
A14: rng(f1/*q)c=dom f2/\left_open_halfline(lim_in+infty f1)
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A15:  (f1/*q).n=x by FUNCT_2:113;
A16:  x=f1.(q.n) by A10,A11,A15,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      r<s.(n+k) by A8,NAT_1:12;
      then s.(n+k) in {r2: r<r2};
      then
A17:  s.(n+k) in right_open_halfline(r) by XXREAL_1:230;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\right_open_halfline(r) by A10,A17,XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim_in+infty f1 by A4;
      then x in {g1: g1<lim_in+infty f1} by A16;
      then
A18:  x in left_open_halfline(lim_in+infty f1) by XXREAL_1:229;
A19:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A13;
      then x in dom f2 by A10,A16,FUNCT_2:108,A19;
      hence thesis by A18,XBOOLE_0:def 4;
    end;
A20: f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A13,VALUED_0:27
      .=((f2*f1)/*s)^\k by A7,VALUED_0:31;
    L=L;
    then
A21: f2/*(f1/*q) is convergent by A2,A12,A14,LIMFUNC2:def 7;
    hence (f2*f1)/*s is convergent by A20,SEQ_4:21;
    lim(f2/*(f1/*q))=L by A2,A12,A14,LIMFUNC2:def 7;
    hence lim((f2*f1)/*s)=L by A21,A20,SEQ_4:22;
  end;
  hence f2*f1 is convergent_in+infty by A3;
  hence thesis by A5,LIMFUNC1:def 12;
end;

theorem
  f1 is convergent_in+infty & f2 is_right_convergent_in lim_in+infty f1
  & (for r ex g st r<g & g in dom(f2*f1)) & (ex r st for g st g in dom f1 /\
  right_open_halfline(r) holds lim_in+infty f1<f1.g) implies f2*f1 is
  convergent_in+infty & lim_in+infty(f2*f1)=lim_right(f2,lim_in+infty f1)
proof
  assume that
A1: f1 is convergent_in+infty and
A2: f2 is_right_convergent_in lim_in+infty f1 and
A3: for r ex g st r<g & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\right_open_halfline(r) holds lim_in+infty f1< f1.g;
A5: now
    set L=lim_right(f2,lim_in+infty f1);
    let s be Real_Sequence;
    assume that
A6: s is divergent_to+infty and
A7: rng s c=dom(f2*f1);
    consider k being Nat such that
A8: for n being Nat st k<=n holds r<s.n by A6;
    set q=s^\k;
A9: q is divergent_to+infty by A6,LIMFUNC1:26;
A10: rng s c=dom f1 by A7,Lm2;
A11: rng q c=rng s by VALUED_0:21;
    then rng q c=dom f1 by A10;
    then
A12: f1/*q is convergent & lim(f1/*q)=lim_in+infty f1 by A1,A9,
LIMFUNC1:def 12;
A13: rng(f1/*s)c=dom f2 by A7,Lm2;
A14: rng(f1/*q)c=dom f2/\right_open_halfline(lim_in+infty f1)
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A15:  (f1/*q).n=x by FUNCT_2:113;
A16:  x=f1.(q.n) by A10,A11,A15,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      r<s.(n+k) by A8,NAT_1:12;
      then s.(n+k) in {r2: r<r2};
      then
A17:  s.(n+k) in right_open_halfline(r) by XXREAL_1:230;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\right_open_halfline(r) by A10,A17,XBOOLE_0:def 4;
      then lim_in+infty f1<f1.(s.(n+k)) by A4;
      then x in {g1: lim_in+infty f1<g1} by A16;
      then
A18:  x in right_open_halfline(lim_in+infty f1) by XXREAL_1:230;
A19:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A13;
      then x in dom f2 by A10,A16,FUNCT_2:108,A19;
      hence thesis by A18,XBOOLE_0:def 4;
    end;
A20: f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A13,VALUED_0:27
      .=((f2*f1)/*s)^\k by A7,VALUED_0:31;
    L=L;
    then
A21: f2/*(f1/*q) is convergent by A2,A12,A14,LIMFUNC2:def 8;
    hence (f2*f1)/*s is convergent by A20,SEQ_4:21;
    lim(f2/*(f1/*q))=L by A2,A12,A14,LIMFUNC2:def 8;
    hence lim((f2*f1)/*s)=L by A21,A20,SEQ_4:22;
  end;
  hence f2*f1 is convergent_in+infty by A3;
  hence thesis by A5,LIMFUNC1:def 12;
end;

theorem
  f1 is convergent_in-infty & f2 is_left_convergent_in lim_in-infty f1 &
  (for r ex g st g<r & g in dom(f2*f1)) & (ex r st for g st g in dom f1 /\
  left_open_halfline(r) holds f1.g<lim_in-infty f1) implies f2*f1 is
  convergent_in-infty & lim_in-infty(f2*f1)=lim_left(f2,lim_in-infty f1)
proof
  assume that
A1: f1 is convergent_in-infty and
A2: f2 is_left_convergent_in lim_in-infty f1 and
A3: for r ex g st g<r & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\left_open_halfline(r) holds f1.g<lim_in-infty f1;
A5: now
    set L=lim_left(f2,lim_in-infty f1);
    let s be Real_Sequence;
    assume that
A6: s is divergent_to-infty and
A7: rng s c=dom(f2*f1);
    consider k being Nat such that
A8: for n being Nat st k<=n holds s.n<r by A6;
    set q=s^\k;
A9: q is divergent_to-infty by A6,LIMFUNC1:27;
A10: rng s c=dom f1 by A7,Lm2;
A11: rng q c=rng s by VALUED_0:21;
    then rng q c=dom f1 by A10;
    then
A12: f1/*q is convergent & lim(f1/*q)=lim_in-infty f1 by A1,A9,
LIMFUNC1:def 13;
A13: rng(f1/*s)c=dom f2 by A7,Lm2;
A14: rng(f1/*q)c=dom f2/\left_open_halfline(lim_in-infty f1)
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A15:  (f1/*q).n=x by FUNCT_2:113;
A16:  x=f1.(q.n) by A10,A11,A15,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      s.(n+k)<r by A8,NAT_1:12;
      then s.(n+k) in {r2: r2<r};
      then
A17:  s.(n+k) in left_open_halfline(r) by XXREAL_1:229;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\left_open_halfline(r) by A10,A17,XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim_in-infty f1 by A4;
      then x in {g1: g1<lim_in-infty f1} by A16;
      then
A18:  x in left_open_halfline(lim_in-infty f1) by XXREAL_1:229;
A19:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A13;
      then x in dom f2 by A10,A16,FUNCT_2:108,A19;
      hence thesis by A18,XBOOLE_0:def 4;
    end;
A20: f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A13,VALUED_0:27
      .=((f2*f1)/*s)^\k by A7,VALUED_0:31;
    L=L;
    then
A21: f2/*(f1/*q) is convergent by A2,A12,A14,LIMFUNC2:def 7;
    hence (f2*f1)/*s is convergent by A20,SEQ_4:21;
    lim(f2/*(f1/*q))=L by A2,A12,A14,LIMFUNC2:def 7;
    hence lim((f2*f1)/*s)=L by A21,A20,SEQ_4:22;
  end;
  hence f2*f1 is convergent_in-infty by A3;
  hence thesis by A5,LIMFUNC1:def 13;
end;

theorem
  f1 is convergent_in-infty & f2 is_right_convergent_in lim_in-infty f1
  & (for r ex g st g<r & g in dom(f2*f1)) & (ex r st for g st g in dom f1 /\
  left_open_halfline(r) holds lim_in-infty f1<f1.g) implies f2*f1 is
  convergent_in-infty & lim_in-infty(f2*f1)=lim_right(f2,lim_in-infty f1)
proof
  assume that
A1: f1 is convergent_in-infty and
A2: f2 is_right_convergent_in lim_in-infty f1 and
A3: for r ex g st g<r & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\left_open_halfline(r) holds lim_in-infty f1<f1 .g;
A5: now
    set L=lim_right(f2,lim_in-infty f1);
    let s be Real_Sequence;
    assume that
A6: s is divergent_to-infty and
A7: rng s c=dom(f2*f1);
    consider k being Nat such that
A8: for n being Nat st k<=n holds s.n<r by A6;
    set q=s^\k;
A9: q is divergent_to-infty by A6,LIMFUNC1:27;
A10: rng s c=dom f1 by A7,Lm2;
A11: rng q c=rng s by VALUED_0:21;
    then rng q c=dom f1 by A10;
    then
A12: f1/*q is convergent & lim(f1/*q)=lim_in-infty f1 by A1,A9,
LIMFUNC1:def 13;
A13: rng(f1/*s)c=dom f2 by A7,Lm2;
A14: rng(f1/*q)c=dom f2/\right_open_halfline(lim_in-infty f1)
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A15:  (f1/*q).n=x by FUNCT_2:113;
A16:  x=f1.(q.n) by A10,A11,A15,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      s.(n+k)<r by A8,NAT_1:12;
      then s.(n+k) in {r2: r2<r};
      then
A17:  s.(n+k) in left_open_halfline(r) by XXREAL_1:229;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\left_open_halfline(r) by A10,A17,XBOOLE_0:def 4;
      then lim_in-infty f1<f1.(s.(n+k)) by A4;
      then x in {g1: lim_in-infty f1<g1} by A16;
      then
A18:  x in right_open_halfline(lim_in-infty f1) by XXREAL_1:230;
A19:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A13;
      then x in dom f2 by A10,A16,FUNCT_2:108,A19;
      hence thesis by A18,XBOOLE_0:def 4;
    end;
A20: f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A13,VALUED_0:27
      .=((f2*f1)/*s)^\k by A7,VALUED_0:31;
    L=L;
    then
A21: f2/*(f1/*q) is convergent by A2,A12,A14,LIMFUNC2:def 8;
    hence (f2*f1)/*s is convergent by A20,SEQ_4:21;
    lim(f2/*(f1/*q))=L by A2,A12,A14,LIMFUNC2:def 8;
    hence lim((f2*f1)/*s)=L by A21,A20,SEQ_4:22;
  end;
  hence f2*f1 is convergent_in-infty by A3;
  hence thesis by A5,LIMFUNC1:def 13;
end;

theorem
  f1 is_divergent_to+infty_in x0 & f2 is convergent_in+infty & (for r1,
r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2<r2 & x0<
  g2 & g2 in dom(f2*f1)) implies f2*f1 is_convergent_in x0 & lim(f2*f1,x0)=
  lim_in+infty f2
proof
  assume that
A1: f1 is_divergent_to+infty_in x0 and
A2: f2 is convergent_in+infty and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
A4: now
    let s be Real_Sequence;
    assume that
A5: s is convergent & lim s=x0 and
A6: rng s c=dom(f2*f1)\{x0};
    rng s c=dom f1\{x0} by A6,Th2;
    then
A7: f1/*s is divergent_to+infty by A1,A5,LIMFUNC3:def 2;
A8: rng(f1/*s)c=dom f2 by A6,Th2;
    then
A9: lim(f2/*(f1/*s))=lim_in+infty f2 by A2,A7,LIMFUNC1:def 12;
A10: rng s c=dom(f2*f1) by A6,Th2;
    f2/*(f1/*s) is convergent by A2,A8,A7;
    hence (f2*f1)/*s is convergent & lim((f2*f1)/*s)=lim_in+infty f2 by A10,A9,
VALUED_0:31;
  end;
  hence f2*f1 is_convergent_in x0 by A3,LIMFUNC3:def 1;
  hence thesis by A4,LIMFUNC3:def 4;
end;

theorem
  f1 is_divergent_to-infty_in x0 & f2 is convergent_in-infty & (for r1,
r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2<r2 & x0<
  g2 & g2 in dom(f2*f1)) implies f2*f1 is_convergent_in x0 & lim(f2*f1,x0)=
  lim_in-infty f2
proof
  assume that
A1: f1 is_divergent_to-infty_in x0 and
A2: f2 is convergent_in-infty and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
A4: now
    let s be Real_Sequence;
    assume that
A5: s is convergent & lim s=x0 and
A6: rng s c=dom(f2*f1)\{x0};
    rng s c=dom f1\{x0} by A6,Th2;
    then
A7: f1/*s is divergent_to-infty by A1,A5,LIMFUNC3:def 3;
A8: rng(f1/*s)c=dom f2 by A6,Th2;
    then
A9: lim(f2/*(f1/*s))=lim_in-infty f2 by A2,A7,LIMFUNC1:def 13;
A10: rng s c=dom(f2*f1) by A6,Th2;
    f2/*(f1/*s) is convergent by A2,A8,A7;
    hence (f2*f1)/*s is convergent & lim((f2*f1)/*s)=lim_in-infty f2 by A10,A9,
VALUED_0:31;
  end;
  hence f2*f1 is_convergent_in x0 by A3,LIMFUNC3:def 1;
  hence thesis by A4,LIMFUNC3:def 4;
end;

theorem
  f1 is convergent_in+infty & f2 is_convergent_in lim_in+infty f1 & (for
  r ex g st r<g & g in dom(f2*f1)) & (ex r st for g st g in dom f1 /\
  right_open_halfline(r) holds f1.g<>lim_in+infty f1) implies f2*f1 is
  convergent_in+infty & lim_in+infty(f2*f1)=lim(f2,lim_in+infty f1)
proof
  assume that
A1: f1 is convergent_in+infty and
A2: f2 is_convergent_in lim_in+infty f1 and
A3: for r ex g st r<g & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\right_open_halfline(r) holds f1.g<> lim_in+infty f1;
A5: now
    set L=lim(f2,lim_in+infty f1);
    let s be Real_Sequence;
    assume that
A6: s is divergent_to+infty and
A7: rng s c=dom(f2*f1);
    consider k being Nat such that
A8: for n being Nat st k<=n holds r<s.n by A6;
    set q=s^\k;
A9: q is divergent_to+infty by A6,LIMFUNC1:26;
A10: rng s c=dom f1 by A7,Lm2;
A11: rng q c=rng s by VALUED_0:21;
    then rng q c=dom f1 by A10;
    then
A12: f1/*q is convergent & lim(f1/*q)=lim_in+infty f1 by A1,A9,
LIMFUNC1:def 12;
A13: rng(f1/*s)c=dom f2 by A7,Lm2;
A14: rng(f1/*q)c=dom f2\{lim_in+infty f1}
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A15:  (f1/*q).n=x by FUNCT_2:113;
A16:  x=f1.(q.n) by A10,A11,A15,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      r<s.(n+k) by A8,NAT_1:12;
      then s.(n+k) in {r2: r<r2};
      then
A17:  s.(n+k) in right_open_halfline(r) by XXREAL_1:230;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\right_open_halfline(r) by A10,A17,XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim_in+infty f1 by A4;
      then
A18:  not f1.(s.(n+k)) in {lim_in+infty f1} by TARSKI:def 1;
A19:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A13;
      then x in dom f2 by A10,A16,FUNCT_2:108,A19;
      hence thesis by A16,A18,XBOOLE_0:def 5;
    end;
A20: f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A13,VALUED_0:27
      .=((f2*f1)/*s)^\k by A7,VALUED_0:31;
    L=L;
    then
A21: f2/*(f1/*q) is convergent by A2,A12,A14,LIMFUNC3:def 4;
    hence (f2*f1)/*s is convergent by A20,SEQ_4:21;
    lim(f2/*(f1/*q))=L by A2,A12,A14,LIMFUNC3:def 4;
    hence lim((f2*f1)/*s)=L by A21,A20,SEQ_4:22;
  end;
  hence f2*f1 is convergent_in+infty by A3;
  hence thesis by A5,LIMFUNC1:def 12;
end;

theorem
  f1 is convergent_in-infty & f2 is_convergent_in lim_in-infty f1 & (for
  r ex g st g<r & g in dom(f2*f1)) & (ex r st for g st g in dom f1 /\
  left_open_halfline(r) holds f1.g<>lim_in-infty f1) implies f2*f1 is
  convergent_in-infty & lim_in-infty(f2*f1)=lim(f2,lim_in-infty f1)
proof
  assume that
A1: f1 is convergent_in-infty and
A2: f2 is_convergent_in lim_in-infty f1 and
A3: for r ex g st g<r & g in dom(f2*f1);
  given r such that
A4: for g st g in dom f1/\left_open_halfline(r) holds f1.g<>lim_in-infty f1;
A5: now
    set L=lim(f2,lim_in-infty f1);
    let s be Real_Sequence;
    assume that
A6: s is divergent_to-infty and
A7: rng s c=dom(f2*f1);
    consider k being Nat such that
A8: for n being Nat st k<=n holds s.n<r by A6;
    set q=s^\k;
A9: q is divergent_to-infty by A6,LIMFUNC1:27;
A10: rng s c=dom f1 by A7,Lm2;
A11: rng q c=rng s by VALUED_0:21;
    then rng q c=dom f1 by A10;
    then
A12: f1/*q is convergent & lim(f1/*q)=lim_in-infty f1 by A1,A9,
LIMFUNC1:def 13;
A13: rng(f1/*s)c=dom f2 by A7,Lm2;
A14: rng(f1/*q)c=dom f2\{lim_in-infty f1}
    proof
      let x be object;
      assume x in rng(f1/*q);
      then consider n be Element of NAT such that
A15:  (f1/*q).n=x by FUNCT_2:113;
A16:  x=f1.(q.n) by A10,A11,A15,FUNCT_2:108,XBOOLE_1:1
        .=f1.(s.(n+k)) by NAT_1:def 3;
      s.(n+k)<r by A8,NAT_1:12;
      then s.(n+k) in {r2: r2<r};
      then
A17:  s.(n+k) in left_open_halfline(r) by XXREAL_1:229;
      s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in dom f1/\left_open_halfline(r) by A10,A17,XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim_in-infty f1 by A4;
      then
A18:  not f1.(s.(n+k)) in {lim_in-infty f1} by TARSKI:def 1;
A19:   n+k in NAT by ORDINAL1:def 12;
      (f1/*s).(n+k) in rng(f1/*s) by VALUED_0:28;
      then (f1/*s).(n+k) in dom f2 by A13;
      then x in dom f2 by A10,A16,FUNCT_2:108,A19;
      hence thesis by A16,A18,XBOOLE_0:def 5;
    end;
A20: f2/*(f1/*q)=f2/*((f1/*s)^\k) by A10,VALUED_0:27
      .=(f2/*(f1/*s))^\k by A13,VALUED_0:27
      .=((f2*f1)/*s)^\k by A7,VALUED_0:31;
    L=L;
    then
A21: f2/*(f1/*q) is convergent by A2,A12,A14,LIMFUNC3:def 4;
    hence (f2*f1)/*s is convergent by A20,SEQ_4:21;
    lim(f2/*(f1/*q))=L by A2,A12,A14,LIMFUNC3:def 4;
    hence lim((f2*f1)/*s)=L by A21,A20,SEQ_4:22;
  end;
  hence f2*f1 is convergent_in-infty by A3;
  hence thesis by A5,LIMFUNC1:def 13;
end;

theorem
  f1 is_convergent_in x0 & f2 is_left_convergent_in lim(f1,x0) & (for r1
,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2<r2 & x0<
g2 & g2 in dom(f2*f1)) & (ex g st 0<g & for r st r in dom f1 /\ (].x0-g,x0.[ \/
].x0,x0+g.[) holds f1.r<lim(f1,x0)) implies f2*f1 is_convergent_in x0 & lim(f2*
  f1,x0)=lim_left(f2,lim(f1,x0))
proof
  assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_left_convergent_in lim(f1,x0) and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) holds f1.r<lim(f1, x0);
A6: now
    let s be Real_Sequence;
    assume that
A7: s is convergent & lim s=x0 and
A8: rng s c=dom(f2*f1)\{x0};
    consider k being Element of NAT such that
A9: for n being Element of NAT st k<=n holds x0-g<s.n & s.n<x0+g by A4,A7,
LIMFUNC3:7;
    set q=(f1/*s)^\k;
A10: rng s c=dom(f2*f1) by A8,Th2;
A11: rng s c=dom f1 by A8,Th2;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A12:  q.n=x by FUNCT_2:113;
A13:  f1.(s.(n+k))=(f1/*s).(n+k) by A11,FUNCT_2:108
        .=x by A12,NAT_1:def 3;
      k<=n+k by NAT_1:12;
      then x0-g<s.(n+k) & s.(n+k)<x0+g by A9;
      then s.(n+k) in {g1: x0-g<g1 & g1<x0+g};
      then
A14:  s.(n+k) in ].x0-g,x0+g.[ by RCOMP_1:def 2;
A15:  s.(n+k) in rng s by VALUED_0:28;
      then not s.(n+k) in {x0} by A8,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0+g.[\{x0} by A14,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0.[\/].x0,x0+g.[ by A4,LIMFUNC3:4;
      then s.(n+k) in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) by A11,A15,
XBOOLE_0:def 4;
      then f1.(s.(n+k))<lim(f1,x0) by A5;
      then f1.(s.(n+k)) in {g2: g2<lim(f1,x0)};
      then
A16:  f1.(s.(n+k)) in left_open_halfline(lim(f1,x0)) by XXREAL_1:229;
      f1.(s.(n+k)) in dom f2 by A10,A15,FUNCT_1:11;
      hence x in dom f2/\left_open_halfline(lim(f1,x0)) by A16,A13,
XBOOLE_0:def 4;
    end;
    then
A17: rng q c=dom f2/\ left_open_halfline(lim(f1,x0));
    rng(f1/*s)c=dom f2 by A8,Th2;
    then
A18: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A10,VALUED_0:31;
A19: rng s c=dom f1\{x0} by A8,Th2;
    then
A20: f1/*s is convergent by A1,A2,A7,LIMFUNC3:def 4;
    lim(f1/*s)=lim(f1,x0) by A1,A7,A19,LIMFUNC3:def 4;
    then
A21: lim q=lim(f1,x0) by A20,SEQ_4:20;
    lim_left(f2,lim(f1,x0))=lim_left(f2,lim(f1,x0));
    then
A22: f2/*q is convergent by A2,A20,A21,A17,LIMFUNC2:def 7;
    hence (f2*f1)/*s is convergent by A18,SEQ_4:21;
    lim(f2/*q)=lim_left(f2,lim(f1,x0)) by A2,A20,A21,A17,LIMFUNC2:def 7;
    hence lim((f2*f1)/*s)=lim_left(f2,lim(f1,x0)) by A22,A18,SEQ_4:22;
  end;
  hence f2*f1 is_convergent_in x0 by A3,LIMFUNC3:def 1;
  hence thesis by A6,LIMFUNC3:def 4;
end;

theorem
  f1 is_left_convergent_in x0 & f2 is_convergent_in lim_left(f1,x0) & (
for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1)) & (ex g st 0<g & for r st r
  in dom f1 /\ ].x0-g,x0.[ holds f1.r<>lim_left(f1,x0)) implies f2*f1
  is_left_convergent_in x0 & lim_left(f2*f1,x0)=lim(f2,lim_left(f1,x0))
proof
  assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_convergent_in lim_left(f1,x0) and
A3: for r st r<x0 ex g st r<g & g<x0 & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0-g,x0.[ holds f1.r<>lim_left(f1,x0);
A6: now
    let s be Real_Sequence;
    assume that
A7: s is convergent & lim s=x0 and
A8: rng s c=dom(f2*f1)/\left_open_halfline(x0);
    consider k being Nat such that
A9: for n being Nat st k<=n holds x0-g<s.n by A4,A7,Lm1,LIMFUNC2:1;
A10: rng s c=dom f1 by A8,Th1;
    set q=(f1/*s)^\k;
A11: rng s c=dom(f2*f1) by A8,Th1;
A12: rng s c=left_open_halfline(x0) by A8,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A13:  q.n=x by FUNCT_2:113;
A14:   n+k in NAT by ORDINAL1:def 12;
A15:  f1.(s.(n+k))=(f1/*s).(n+k) by A10,FUNCT_2:108,A14
        .=x by A13,NAT_1:def 3;
A16:  x0-g<s.(n+k) by A9,NAT_1:12;
A17:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in left_open_halfline(x0) by A12;
      then s.(n+k) in {g1: g1<x0} by XXREAL_1:229;
      then ex g1 st g1=s.(n+k) & g1<x0;
      then s.(n+k) in {g2: x0-g<g2 & g2<x0} by A16;
      then s.(n+k) in ].x0-g,x0.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0-g,x0.[ by A10,A17,XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim_left(f1,x0) by A5;
      then
A18:  not f1.(s.(n+k)) in {lim_left(f1,x0)} by TARSKI:def 1;
      f1.(s.(n+k)) in dom f2 by A11,A17,FUNCT_1:11;
      hence x in dom f2\{lim_left(f1,x0)} by A18,A15,XBOOLE_0:def 5;
    end;
    then
A19: rng q c=dom f2\{lim_left(f1,x0)};
    rng(f1/*s)c=dom f2 by A8,Th1;
    then
A20: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A11,VALUED_0:31;
A21: rng s c=dom f1/\left_open_halfline(x0) by A8,Th1;
    then
A22: f1/*s is convergent by A1,A2,A7,LIMFUNC2:def 7;
    lim(f1/*s)=lim_left(f1,x0) by A1,A7,A21,LIMFUNC2:def 7;
    then
A23: lim q=lim_left(f1,x0) by A22,SEQ_4:20;
    lim(f2,lim_left(f1,x0))=lim(f2,lim_left(f1,x0));
    then
A24: f2/*q is convergent by A2,A22,A23,A19,LIMFUNC3:def 4;
    hence (f2*f1)/*s is convergent by A20,SEQ_4:21;
    lim(f2/*q)=lim(f2,lim_left(f1,x0)) by A2,A22,A23,A19,LIMFUNC3:def 4;
    hence lim((f2*f1)/*s)=lim(f2,lim_left(f1,x0)) by A24,A20,SEQ_4:22;
  end;
  hence f2*f1 is_left_convergent_in x0 by A3,LIMFUNC2:def 1;
  hence thesis by A6,LIMFUNC2:def 7;
end;

theorem
  f1 is_convergent_in x0 & f2 is_right_convergent_in lim(f1,x0) & (for
  r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2<r2 &
x0<g2 & g2 in dom(f2*f1)) & (ex g st 0<g & for r st r in dom f1 /\ (].x0-g,x0.[
\/ ].x0,x0+g.[) holds lim(f1,x0)<f1.r) implies f2*f1 is_convergent_in x0 & lim(
  f2*f1,x0)=lim_right(f2,lim(f1,x0))
proof
  assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_right_convergent_in lim(f1,x0) and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) holds lim(f1,x0)<f1 .r;
A6: now
    let s be Real_Sequence;
    assume that
A7: s is convergent & lim s=x0 and
A8: rng s c=dom(f2*f1)\{x0};
    consider k being Element of NAT such that
A9: for n being Element of NAT st k<=n holds x0-g<s.n & s.n<x0+g by A4,A7,
LIMFUNC3:7;
    set q=(f1/*s)^\k;
A10: rng s c=dom(f2*f1) by A8,Th2;
A11: rng s c=dom f1 by A8,Th2;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A12:  q.n=x by FUNCT_2:113;
A13:  f1.(s.(n+k))=(f1/*s).(n+k) by A11,FUNCT_2:108
        .=x by A12,NAT_1:def 3;
      k<=n+k by NAT_1:12;
      then x0-g<s.(n+k) & s.(n+k)<x0+g by A9;
      then s.(n+k) in {g1: x0-g<g1 & g1<x0+g};
      then
A14:  s.(n+k) in ].x0-g,x0+g.[ by RCOMP_1:def 2;
A15:  s.(n+k) in rng s by VALUED_0:28;
      then not s.(n+k) in {x0} by A8,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0+g.[\{x0} by A14,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0.[\/].x0,x0+g.[ by A4,LIMFUNC3:4;
      then s.(n+k) in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) by A11,A15,
XBOOLE_0:def 4;
      then f1.(s.(n+k))>lim(f1,x0) by A5;
      then f1.(s.(n+k)) in {g2: lim(f1,x0)<g2};
      then
A16:  f1.(s.(n+k)) in right_open_halfline(lim(f1,x0)) by XXREAL_1:230;
      f1.(s.(n+k)) in dom f2 by A10,A15,FUNCT_1:11;
      hence x in dom f2/\right_open_halfline(lim(f1,x0)) by A16,A13,
XBOOLE_0:def 4;
    end;
    then
A17: rng q c=dom f2/\right_open_halfline(lim(f1,x0));
    rng(f1/*s)c=dom f2 by A8,Th2;
    then
A18: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A10,VALUED_0:31;
A19: rng s c=dom f1\{x0} by A8,Th2;
    then
A20: f1/*s is convergent by A1,A2,A7,LIMFUNC3:def 4;
    lim(f1/*s)=lim(f1,x0) by A1,A7,A19,LIMFUNC3:def 4;
    then
A21: lim q=lim(f1,x0) by A20,SEQ_4:20;
    lim_right(f2,lim(f1,x0))=lim_right(f2,lim(f1,x0));
    then
A22: f2/*q is convergent by A2,A20,A21,A17,LIMFUNC2:def 8;
    hence (f2*f1)/*s is convergent by A18,SEQ_4:21;
    lim(f2/*q)=lim_right(f2,lim(f1,x0)) by A2,A20,A21,A17,LIMFUNC2:def 8;
    hence lim((f2*f1)/*s)=lim_right(f2,lim(f1,x0)) by A22,A18,SEQ_4:22;
  end;
  hence f2*f1 is_convergent_in x0 by A3,LIMFUNC3:def 1;
  hence thesis by A6,LIMFUNC3:def 4;
end;

theorem
  f1 is_right_convergent_in x0 & f2 is_convergent_in lim_right(f1,x0) &
(for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1)) & (ex g st 0<g & for r st
  r in dom f1 /\ ].x0,x0+g.[ holds f1.r<>lim_right(f1,x0)) implies f2*f1
  is_right_convergent_in x0 & lim_right(f2*f1,x0)=lim(f2,lim_right(f1,x0))
proof
  assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_convergent_in lim_right(f1,x0) and
A3: for r st x0<r ex g st g<r & x0<g & g in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\].x0,x0+g.[ holds f1.r<>lim_right(f1,x0);
A6: now
    let s be Real_Sequence;
    assume that
A7: s is convergent & lim s=x0 and
A8: rng s c=dom(f2*f1)/\right_open_halfline(x0);
    consider k being Nat such that
A9: for n being Nat st k<=n holds s.n<x0+g by A4,A7,Lm1,LIMFUNC2:2;
A10: rng s c=dom f1 by A8,Th1;
    set q=(f1/*s)^\k;
A11: rng s c=dom(f2*f1) by A8,Th1;
A12: rng s c=right_open_halfline(x0) by A8,Th1;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A13:  q.n=x by FUNCT_2:113;
A14:   n+k in NAT by ORDINAL1:def 12;
A15:  f1.(s.(n+k))=(f1/*s).(n+k) by A10,FUNCT_2:108,A14
        .=x by A13,NAT_1:def 3;
A16:  s.(n+k)<x0+g by A9,NAT_1:12;
A17:  s.(n+k) in rng s by VALUED_0:28;
      then s.(n+k) in right_open_halfline(x0) by A12;
      then s.(n+k) in {g1: x0<g1} by XXREAL_1:230;
      then ex g1 st g1=s.(n+k) & x0<g1;
      then s.(n+k) in {g2: x0<g2 & g2<x0+g} by A16;
      then s.(n+k) in ].x0,x0+g.[ by RCOMP_1:def 2;
      then s.(n+k) in dom f1/\].x0,x0+g.[ by A10,A17,XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim_right(f1,x0) by A5;
      then
A18:  not f1.(s.(n+k)) in {lim_right(f1,x0)} by TARSKI:def 1;
      f1.(s.(n+k)) in dom f2 by A11,A17,FUNCT_1:11;
      hence x in dom f2\{lim_right(f1,x0)} by A18,A15,XBOOLE_0:def 5;
    end;
    then
A19: rng q c=dom f2\{lim_right(f1,x0)};
    rng(f1/*s)c=dom f2 by A8,Th1;
    then
A20: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A11,VALUED_0:31;
A21: rng s c=dom f1/\right_open_halfline(x0) by A8,Th1;
    then
A22: f1/*s is convergent by A1,A2,A7,LIMFUNC2:def 8;
    lim(f1/*s)=lim_right(f1,x0) by A1,A7,A21,LIMFUNC2:def 8;
    then
A23: lim q=lim_right(f1,x0) by A22,SEQ_4:20;
    lim(f2,lim_right(f1,x0))=lim(f2,lim_right(f1,x0));
    then
A24: f2/*q is convergent by A2,A22,A23,A19,LIMFUNC3:def 4;
    hence (f2*f1)/*s is convergent by A20,SEQ_4:21;
    lim(f2/*q)=lim(f2,lim_right(f1,x0)) by A2,A22,A23,A19,LIMFUNC3:def 4;
    hence lim((f2*f1)/*s)=lim(f2,lim_right(f1,x0)) by A24,A20,SEQ_4:22;
  end;
  hence f2*f1 is_right_convergent_in x0 by A3,LIMFUNC2:def 4;
  hence thesis by A6,LIMFUNC2:def 8;
end;

theorem
  f1 is_convergent_in x0 & f2 is_convergent_in lim(f1,x0) & (for r1,r2
st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*f1) & g2<r2 & x0<g2 &
g2 in dom(f2*f1)) & (ex g st 0<g & for r st r in dom f1 /\ (].x0-g,x0.[ \/ ].x0
,x0+g.[) holds f1.r<>lim(f1,x0)) implies f2*f1 is_convergent_in x0 & lim(f2*f1,
  x0)=lim(f2,lim(f1,x0))
proof
  assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_convergent_in lim(f1,x0) and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f2*
  f1) & g2<r2 & x0<g2 & g2 in dom(f2*f1);
  given g such that
A4: 0<g and
A5: for r st r in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) holds f1.r<>lim(f1, x0);
A6: now
    let s be Real_Sequence;
    assume that
A7: s is convergent & lim s=x0 and
A8: rng s c=dom(f2*f1)\{x0};
    consider k being Element of NAT such that
A9: for n being Element of NAT st k<=n holds x0-g<s.n & s.n<x0+g by A4,A7,
LIMFUNC3:7;
    set q=(f1/*s)^\k;
A10: rng s c=dom(f2*f1) by A8,Th2;
A11: rng s c=dom f1 by A8,Th2;
    now
      let x be object;
      assume x in rng q;
      then consider n be Element of NAT such that
A12:  q.n=x by FUNCT_2:113;
A13:  f1.(s.(n+k))=(f1/*s).(n+k) by A11,FUNCT_2:108
        .=x by A12,NAT_1:def 3;
      k<=n+k by NAT_1:12;
      then x0-g<s.(n+k) & s.(n+k)<x0+g by A9;
      then s.(n+k) in {g1: x0-g<g1 & g1<x0+g};
      then
A14:  s.(n+k) in ].x0-g,x0+g.[ by RCOMP_1:def 2;
A15:  s.(n+k) in rng s by VALUED_0:28;
      then not s.(n+k) in {x0} by A8,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0+g.[\{x0} by A14,XBOOLE_0:def 5;
      then s.(n+k) in ].x0-g,x0.[\/].x0,x0+g.[ by A4,LIMFUNC3:4;
      then s.(n+k) in dom f1/\(].x0-g,x0.[\/].x0,x0+g.[) by A11,A15,
XBOOLE_0:def 4;
      then f1.(s.(n+k))<>lim(f1,x0) by A5;
      then
A16:  not f1.(s.(n+k)) in {lim(f1,x0)} by TARSKI:def 1;
      f1.(s.(n+k)) in dom f2 by A10,A15,FUNCT_1:11;
      hence x in dom f2\{lim(f1,x0)} by A16,A13,XBOOLE_0:def 5;
    end;
    then
A17: rng q c=dom f2\{lim(f1,x0)};
    rng(f1/*s)c=dom f2 by A8,Th2;
    then
A18: f2/*q=(f2/*(f1/*s))^\k by VALUED_0:27
      .=((f2*f1)/*s)^\k by A10,VALUED_0:31;
A19: rng s c=dom f1\{x0} by A8,Th2;
    then
A20: f1/*s is convergent by A1,A2,A7,LIMFUNC3:def 4;
    lim(f1/*s)=lim(f1,x0) by A1,A7,A19,LIMFUNC3:def 4;
    then
A21: lim q=lim(f1,x0) by A20,SEQ_4:20;
    lim(f2,lim(f1,x0))=lim(f2,lim(f1,x0));
    then
A22: f2/*q is convergent by A2,A20,A21,A17,LIMFUNC3:def 4;
    hence (f2*f1)/*s is convergent by A18,SEQ_4:21;
    lim(f2/*q)=lim(f2,lim(f1,x0)) by A2,A20,A21,A17,LIMFUNC3:def 4;
    hence lim((f2*f1)/*s)=lim(f2,lim(f1,x0)) by A22,A18,SEQ_4:22;
  end;
  hence f2*f1 is_convergent_in x0 by A3,LIMFUNC3:def 1;
  hence thesis by A6,LIMFUNC3:def 4;
end;