:: The Limit of a Composition of Real Functions
:: by Jaros{\l}aw Kotowicz
::
:: Received September 5, 1990
:: Copyright (c) 1990-2021 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;