Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### The Limit of a Composition of Real Functions

by
Jaroslaw Kotowicz

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));
```