:: The Limit of a Composition of Real Functions
:: by Jaros{\l}aw Kotowicz
::
:: Received September 5, 1990
:: Copyright (c) 1990-2025 Association of Mizar Users


Lm1: for r, g being Real st 0 < g holds
( r - g < r & r < r + g )
proof end;

Lm2: for f1, f2 being PartFunc of REAL,REAL
for s being Real_Sequence st rng s c= dom (f2 * f1) holds
( rng s c= dom f1 & rng (f1 /* s) c= dom f2 )
proof end;

theorem Th1: :: LIMFUNC4:1
for f1, f2 being PartFunc of REAL,REAL
for s being Real_Sequence
for X being 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 end;

theorem Th2: :: LIMFUNC4:2
for f1, f2 being PartFunc of REAL,REAL
for s being Real_Sequence
for X being 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 end;

theorem :: LIMFUNC4:3
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) holds
f2 * f1 is divergent_in+infty_to+infty
proof end;

theorem :: LIMFUNC4:4
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to-infty & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) holds
f2 * f1 is divergent_in+infty_to-infty
proof end;

theorem :: LIMFUNC4:5
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & f2 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) holds
f2 * f1 is divergent_in+infty_to+infty
proof end;

theorem :: LIMFUNC4:6
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & f2 is divergent_in-infty_to-infty & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) holds
f2 * f1 is divergent_in+infty_to-infty
proof end;

theorem :: LIMFUNC4:7
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & f2 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) holds
f2 * f1 is divergent_in-infty_to+infty
proof end;

theorem :: LIMFUNC4:8
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & f2 is divergent_in+infty_to-infty & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) holds
f2 * f1 is divergent_in-infty_to-infty
proof end;

theorem :: LIMFUNC4:9
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) holds
f2 * f1 is divergent_in-infty_to+infty
proof end;

theorem :: LIMFUNC4:10
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to-infty & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) holds
f2 * f1 is divergent_in-infty_to-infty
proof end;

theorem :: LIMFUNC4:11
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & f2 is divergent_in+infty_to+infty & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) holds
f2 * f1 is_left_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:12
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & f2 is divergent_in+infty_to-infty & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) holds
f2 * f1 is_left_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:13
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to-infty_in x0 & f2 is divergent_in-infty_to+infty & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) holds
f2 * f1 is_left_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:14
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to-infty_in x0 & f2 is divergent_in-infty_to-infty & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) holds
f2 * f1 is_left_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:15
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & f2 is divergent_in+infty_to+infty & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) holds
f2 * f1 is_right_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:16
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & f2 is divergent_in+infty_to-infty & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) holds
f2 * f1 is_right_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:17
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to-infty_in x0 & f2 is divergent_in-infty_to+infty & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) holds
f2 * f1 is_right_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:18
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to-infty_in x0 & f2 is divergent_in-infty_to-infty & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) holds
f2 * f1 is_right_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:19
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_divergent_to+infty_in lim_left (f1,x0) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds
f1 . r < lim_left (f1,x0) ) ) holds
f2 * f1 is_left_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:20
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_divergent_to-infty_in lim_left (f1,x0) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds
f1 . r < lim_left (f1,x0) ) ) holds
f2 * f1 is_left_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:21
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_right_divergent_to+infty_in lim_left (f1,x0) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds
lim_left (f1,x0) < f1 . r ) ) holds
f2 * f1 is_left_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:22
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_right_divergent_to-infty_in lim_left (f1,x0) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds
lim_left (f1,x0) < f1 . r ) ) holds
f2 * f1 is_left_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:23
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_divergent_to+infty_in lim_right (f1,x0) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds
lim_right (f1,x0) < f1 . r ) ) holds
f2 * f1 is_right_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:24
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_divergent_to-infty_in lim_right (f1,x0) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds
lim_right (f1,x0) < f1 . r ) ) holds
f2 * f1 is_right_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:25
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_left_divergent_to+infty_in lim_right (f1,x0) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds
f1 . r < lim_right (f1,x0) ) ) holds
f2 * f1 is_right_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:26
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_left_divergent_to-infty_in lim_right (f1,x0) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds
f1 . r < lim_right (f1,x0) ) ) holds
f2 * f1 is_right_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:27
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_left_divergent_to+infty_in lim_in+infty f1 & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
f1 . g < lim_in+infty f1 holds
f2 * f1 is divergent_in+infty_to+infty
proof end;

theorem :: LIMFUNC4:28
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_left_divergent_to-infty_in lim_in+infty f1 & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
f1 . g < lim_in+infty f1 holds
f2 * f1 is divergent_in+infty_to-infty
proof end;

theorem :: LIMFUNC4:29
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_right_divergent_to+infty_in lim_in+infty f1 & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
lim_in+infty f1 < f1 . g holds
f2 * f1 is divergent_in+infty_to+infty
proof end;

theorem :: LIMFUNC4:30
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_right_divergent_to-infty_in lim_in+infty f1 & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
lim_in+infty f1 < f1 . g holds
f2 * f1 is divergent_in+infty_to-infty
proof end;

theorem :: LIMFUNC4:31
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_left_divergent_to+infty_in lim_in-infty f1 & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g < lim_in-infty f1 holds
f2 * f1 is divergent_in-infty_to+infty
proof end;

theorem :: LIMFUNC4:32
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_left_divergent_to-infty_in lim_in-infty f1 & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g < lim_in-infty f1 holds
f2 * f1 is divergent_in-infty_to-infty
proof end;

theorem :: LIMFUNC4:33
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_right_divergent_to+infty_in lim_in-infty f1 & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
lim_in-infty f1 < f1 . g holds
f2 * f1 is divergent_in-infty_to+infty
proof end;

theorem :: LIMFUNC4:34
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_right_divergent_to-infty_in lim_in-infty f1 & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
lim_in-infty f1 < f1 . g holds
f2 * f1 is divergent_in-infty_to-infty
proof end;

theorem :: LIMFUNC4:35
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to+infty_in x0 & f2 is divergent_in+infty_to+infty & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) holds
f2 * f1 is_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:36
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to+infty_in x0 & f2 is divergent_in+infty_to-infty & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) holds
f2 * f1 is_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:37
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to-infty_in x0 & f2 is divergent_in-infty_to+infty & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) holds
f2 * f1 is_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:38
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to-infty_in x0 & f2 is divergent_in-infty_to-infty & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) holds
f2 * f1 is_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:39
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_divergent_to+infty_in lim (f1,x0) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r <> lim (f1,x0) ) ) holds
f2 * f1 is_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:40
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_divergent_to-infty_in lim (f1,x0) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r <> lim (f1,x0) ) ) holds
f2 * f1 is_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:41
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_right_divergent_to+infty_in lim (f1,x0) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r > lim (f1,x0) ) ) holds
f2 * f1 is_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:42
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_right_divergent_to-infty_in lim (f1,x0) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r > lim (f1,x0) ) ) holds
f2 * f1 is_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:43
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_divergent_to+infty_in lim_right (f1,x0) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds
f1 . r <> lim_right (f1,x0) ) ) holds
f2 * f1 is_right_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:44
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_divergent_to-infty_in lim_right (f1,x0) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds
f1 . r <> lim_right (f1,x0) ) ) holds
f2 * f1 is_right_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:45
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_divergent_to+infty_in lim_in+infty f1 & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
f1 . g <> lim_in+infty f1 holds
f2 * f1 is divergent_in+infty_to+infty
proof end;

theorem :: LIMFUNC4:46
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_divergent_to-infty_in lim_in+infty f1 & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
f1 . g <> lim_in+infty f1 holds
f2 * f1 is divergent_in+infty_to-infty
proof end;

theorem :: LIMFUNC4:47
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_divergent_to+infty_in lim_in-infty f1 & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <> lim_in-infty f1 holds
f2 * f1 is divergent_in-infty_to+infty
proof end;

theorem :: LIMFUNC4:48
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_divergent_to-infty_in lim_in-infty f1 & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <> lim_in-infty f1 holds
f2 * f1 is divergent_in-infty_to-infty
proof end;

theorem :: LIMFUNC4:49
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_left_divergent_to+infty_in lim (f1,x0) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r < lim (f1,x0) ) ) holds
f2 * f1 is_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:50
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_left_divergent_to-infty_in lim (f1,x0) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r < lim (f1,x0) ) ) holds
f2 * f1 is_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:51
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_divergent_to+infty_in lim_left (f1,x0) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds
f1 . r <> lim_left (f1,x0) ) ) holds
f2 * f1 is_left_divergent_to+infty_in x0
proof end;

theorem :: LIMFUNC4:52
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_divergent_to-infty_in lim_left (f1,x0) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds
f1 . r <> lim_left (f1,x0) ) ) holds
f2 * f1 is_left_divergent_to-infty_in x0
proof end;

theorem :: LIMFUNC4:53
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) holds
( f2 * f1 is convergent_in+infty & lim_in+infty (f2 * f1) = lim_in+infty f2 )
proof end;

theorem :: LIMFUNC4:54
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & f2 is convergent_in-infty & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) holds
( f2 * f1 is convergent_in+infty & lim_in+infty (f2 * f1) = lim_in-infty f2 )
proof end;

theorem :: LIMFUNC4:55
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) holds
( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim_in+infty f2 )
proof end;

theorem :: LIMFUNC4:56
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & f2 is convergent_in-infty & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) holds
( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim_in-infty f2 )
proof end;

theorem :: LIMFUNC4:57
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & f2 is convergent_in+infty & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) holds
( f2 * f1 is_left_convergent_in x0 & lim_left ((f2 * f1),x0) = lim_in+infty f2 )
proof end;

theorem :: LIMFUNC4:58
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to-infty_in x0 & f2 is convergent_in-infty & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) holds
( f2 * f1 is_left_convergent_in x0 & lim_left ((f2 * f1),x0) = lim_in-infty f2 )
proof end;

theorem :: LIMFUNC4:59
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & f2 is convergent_in+infty & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) holds
( f2 * f1 is_right_convergent_in x0 & lim_right ((f2 * f1),x0) = lim_in+infty f2 )
proof end;

theorem :: LIMFUNC4:60
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to-infty_in x0 & f2 is convergent_in-infty & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) holds
( f2 * f1 is_right_convergent_in x0 & lim_right ((f2 * f1),x0) = lim_in-infty f2 )
proof end;

theorem :: LIMFUNC4:61
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in lim_left (f1,x0) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds
f1 . r < lim_left (f1,x0) ) ) holds
( f2 * f1 is_left_convergent_in x0 & lim_left ((f2 * f1),x0) = lim_left (f2,(lim_left (f1,x0))) )
proof end;

theorem :: LIMFUNC4:62
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in lim_right (f1,x0) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds
lim_right (f1,x0) < f1 . r ) ) holds
( f2 * f1 is_right_convergent_in x0 & lim_right ((f2 * f1),x0) = lim_right (f2,(lim_right (f1,x0))) )
proof end;

theorem :: LIMFUNC4:63
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_right_convergent_in lim_left (f1,x0) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds
lim_left (f1,x0) < f1 . r ) ) holds
( f2 * f1 is_left_convergent_in x0 & lim_left ((f2 * f1),x0) = lim_right (f2,(lim_left (f1,x0))) )
proof end;

theorem :: LIMFUNC4:64
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_left_convergent_in lim_right (f1,x0) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds
f1 . r < lim_right (f1,x0) ) ) holds
( f2 * f1 is_right_convergent_in x0 & lim_right ((f2 * f1),x0) = lim_left (f2,(lim_right (f1,x0))) )
proof end;

theorem :: LIMFUNC4:65
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_left_convergent_in lim_in+infty f1 & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
f1 . g < lim_in+infty f1 holds
( f2 * f1 is convergent_in+infty & lim_in+infty (f2 * f1) = lim_left (f2,(lim_in+infty f1)) )
proof end;

theorem :: LIMFUNC4:66
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_right_convergent_in lim_in+infty f1 & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
lim_in+infty f1 < f1 . g holds
( f2 * f1 is convergent_in+infty & lim_in+infty (f2 * f1) = lim_right (f2,(lim_in+infty f1)) )
proof end;

theorem :: LIMFUNC4:67
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_left_convergent_in lim_in-infty f1 & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g < lim_in-infty f1 holds
( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim_left (f2,(lim_in-infty f1)) )
proof end;

theorem :: LIMFUNC4:68
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_right_convergent_in lim_in-infty f1 & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
lim_in-infty f1 < f1 . g holds
( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim_right (f2,(lim_in-infty f1)) )
proof end;

theorem :: LIMFUNC4:69
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to+infty_in x0 & f2 is convergent_in+infty & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) holds
( f2 * f1 is_convergent_in x0 & lim ((f2 * f1),x0) = lim_in+infty f2 )
proof end;

theorem :: LIMFUNC4:70
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to-infty_in x0 & f2 is convergent_in-infty & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) holds
( f2 * f1 is_convergent_in x0 & lim ((f2 * f1),x0) = lim_in-infty f2 )
proof end;

theorem :: LIMFUNC4:71
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_convergent_in lim_in+infty f1 & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
f1 . g <> lim_in+infty f1 holds
( f2 * f1 is convergent_in+infty & lim_in+infty (f2 * f1) = lim (f2,(lim_in+infty f1)) )
proof end;

theorem :: LIMFUNC4:72
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_convergent_in lim_in-infty f1 & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <> lim_in-infty f1 holds
( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim (f2,(lim_in-infty f1)) )
proof end;

theorem :: LIMFUNC4:73
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_left_convergent_in lim (f1,x0) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r < lim (f1,x0) ) ) holds
( f2 * f1 is_convergent_in x0 & lim ((f2 * f1),x0) = lim_left (f2,(lim (f1,x0))) )
proof end;

theorem :: LIMFUNC4:74
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_convergent_in lim_left (f1,x0) & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds
f1 . r <> lim_left (f1,x0) ) ) holds
( f2 * f1 is_left_convergent_in x0 & lim_left ((f2 * f1),x0) = lim (f2,(lim_left (f1,x0))) )
proof end;

theorem :: LIMFUNC4:75
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_right_convergent_in lim (f1,x0) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
lim (f1,x0) < f1 . r ) ) holds
( f2 * f1 is_convergent_in x0 & lim ((f2 * f1),x0) = lim_right (f2,(lim (f1,x0))) )
proof end;

theorem :: LIMFUNC4:76
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_convergent_in lim_right (f1,x0) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds
f1 . r <> lim_right (f1,x0) ) ) holds
( f2 * f1 is_right_convergent_in x0 & lim_right ((f2 * f1),x0) = lim (f2,(lim_right (f1,x0))) )
proof end;

theorem :: LIMFUNC4:77
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_convergent_in lim (f1,x0) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st
( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r <> lim (f1,x0) ) ) holds
( f2 * f1 is_convergent_in x0 & lim ((f2 * f1),x0) = lim (f2,(lim (f1,x0))) )
proof end;