The abstract of the Mizar article:

The Limit of a Composition of Real Functions

by

Jaroslaw Kotowicz

Received September 5, 1990

MML identifier: LIMFUNC4

[ Mizar article, MML identifier index ]

environ

 vocabulary PARTFUN1, ARYTM_1, SEQ_1, RELAT_1, FUNCT_1, BOOLE, LIMFUNC1,
      LIMFUNC2, SEQ_2, ORDINAL2, RCOMP_1, SEQM_3, LIMFUNC3;
 notation TARSKI, XBOOLE_0, NUMBERS, XREAL_0, REAL_1, NAT_1, SEQ_1, SEQ_2,
      SEQM_3, RCOMP_1, RELSET_1, PARTFUN1, RFUNCT_2, LIMFUNC1, LIMFUNC2,
      LIMFUNC3;
 constructors REAL_1, NAT_1, SEQ_2, SEQM_3, PROB_1, RCOMP_1, PARTFUN1,
      RFUNCT_2, LIMFUNC1, LIMFUNC2, LIMFUNC3, MEMBERED, XBOOLE_0;
 clusters RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin

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

theorem :: LIMFUNC4:1
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;

theorem :: LIMFUNC4:2
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;

theorem :: LIMFUNC4:3
  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;

theorem :: LIMFUNC4:4
  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;

theorem :: LIMFUNC4:5
  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;

theorem :: LIMFUNC4:6
  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;

theorem :: LIMFUNC4:7
  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;

theorem :: LIMFUNC4:8
  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;

theorem :: LIMFUNC4:9
  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;

theorem :: LIMFUNC4:10
  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;

theorem :: LIMFUNC4:11
  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;

theorem :: LIMFUNC4:12
  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;

theorem :: LIMFUNC4:13
  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;

theorem :: LIMFUNC4:14
  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;

theorem :: LIMFUNC4:15
  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;

theorem :: LIMFUNC4:16
  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;

theorem :: LIMFUNC4:17
  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;

theorem :: LIMFUNC4:18
  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;

theorem :: LIMFUNC4:19
  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;

theorem :: LIMFUNC4:20
  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;

theorem :: LIMFUNC4:21
  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;

theorem :: LIMFUNC4:22
  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;

theorem :: LIMFUNC4:23
  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;

theorem :: LIMFUNC4:24
  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;

theorem :: LIMFUNC4:25
  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;

theorem :: LIMFUNC4:26
  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;

theorem :: LIMFUNC4:27
  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;

theorem :: LIMFUNC4:28
  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;

theorem :: LIMFUNC4:29
  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;

theorem :: LIMFUNC4:30
  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;

theorem :: LIMFUNC4:31
  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;

theorem :: LIMFUNC4:32
  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;

theorem :: LIMFUNC4:33
  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;

theorem :: LIMFUNC4:34
  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;

theorem :: LIMFUNC4:35
  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;

theorem :: LIMFUNC4:36
  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;

theorem :: LIMFUNC4:37
  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;

theorem :: LIMFUNC4:38
  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;

theorem :: LIMFUNC4:39
  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;

theorem :: LIMFUNC4:40
  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;

theorem :: LIMFUNC4:41
  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;

theorem :: LIMFUNC4:42
  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;

theorem :: LIMFUNC4:43
  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;

theorem :: LIMFUNC4:44
  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;

theorem :: LIMFUNC4:45
  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;

theorem :: LIMFUNC4:46
  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;

theorem :: LIMFUNC4:47
  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;

theorem :: LIMFUNC4:48
  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;

theorem :: LIMFUNC4:49
  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;

theorem :: LIMFUNC4:50
  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;

theorem :: LIMFUNC4:51
  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;

theorem :: LIMFUNC4:52
  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;

theorem :: LIMFUNC4:53
  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;

theorem :: LIMFUNC4:54
  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;

theorem :: LIMFUNC4:55
  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;

theorem :: LIMFUNC4:56
  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;

theorem :: LIMFUNC4:57
  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;

theorem :: LIMFUNC4:58
  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;

theorem :: LIMFUNC4:59
  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;

theorem :: LIMFUNC4:60
  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;

theorem :: LIMFUNC4:61
  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));

theorem :: LIMFUNC4:62
  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));

theorem :: LIMFUNC4:63
  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));

theorem :: LIMFUNC4:64
  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));

theorem :: LIMFUNC4:65
  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);

theorem :: LIMFUNC4:66
  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);

theorem :: LIMFUNC4:67
  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);

theorem :: LIMFUNC4:68
  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);


theorem :: LIMFUNC4:69
  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;

theorem :: LIMFUNC4:70
  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;

theorem :: LIMFUNC4:71
  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);

theorem :: LIMFUNC4:72
  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);

theorem :: LIMFUNC4:73
  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));

theorem :: LIMFUNC4:74
  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));

theorem :: LIMFUNC4:75
  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));

theorem :: LIMFUNC4:76
  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));

theorem :: LIMFUNC4:77
  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));