:: LIMFUNC2 semantic presentation

Lemma1: for b₁, b₂, b₃ being real number st 0 < b₂ & b₁ <= b₃ holds
( b₁ - b₂ < b₃ & b₁ < b₃ + b₂ )

proof end;

Lemma2: for b₁ being Real_Sequence
for b₂, b₃ being PartFunc of REAL , REAL
for b₄ being Subset of REAL st rng b₁ c= (dom (b₂ (#) b₃)) /\ b₄ holds
( rng b₁ c= dom (b₂ (#) b₃) & rng b₁ c= b₄ & dom (b₂ (#) b₃) = (dom b₂) /\ (dom b₃) & rng b₁ c= dom b₂ & rng b₁ c= dom b₃ & rng b₁ c= (dom b₂) /\ b₄ & rng b₁ c= (dom b₃) /\ b₄ )

proof end;

Lemma3: for b₁ being Real
for b₂ being Nat holds
( b₁ - (1 / (b₂ + 1)) < b₁ & b₁ < b₁ + (1 / (b₂ + 1)) )

proof end;

Lemma4: for b₁ being Real_Sequence
for b₂, b₃ being PartFunc of REAL , REAL
for b₄ being Subset of REAL st rng b₁ c= (dom (b₂ + b₃)) /\ b₄ holds
( rng b₁ c= dom (b₂ + b₃) & rng b₁ c= b₄ & dom (b₂ + b₃) = (dom b₂) /\ (dom b₃) & rng b₁ c= (dom b₂) /\ b₄ & rng b₁ c= (dom b₃) /\ b₄ )

proof end;

theorem Th1: :: LIMFUNC2:1

for b₁ being Real
for b₂ being Real_Sequence st b₂ is convergent & b₁ < lim b₂ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
b₁ < b₂ . b₄

proof end;

theorem Th2: :: LIMFUNC2:2

for b₁ being Real
for b₂ being Real_Sequence st b₂ is convergent & lim b₂ < b₁ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
b₂ . b₄ < b₁

proof end;

Lemma7: for b₁ being Real
for b₂ being Real_Sequence
for b₃ being PartFunc of REAL , REAL st ( for b₄ being Real ex b₅ being Real st
( b₁ < b₅ & ( for b₆ being Real st b₆ < b₅ & b₁ < b₆ & b₆ in dom b₃ holds
b₃ . b₆ < b₄ ) ) ) & b₂ is convergent & lim b₂ = b₁ & rng b₂ c= (dom b₃) /\ (right_open_halfline b₁) holds
b₃ * b₂ is divergent_to-infty

proof end;

theorem Th3: :: LIMFUNC2:3

for b₁, b₂ being Real
for b₃ being PartFunc of REAL , REAL st 0 < b₁ & ].(b₂ - b₁),b₂.[ c= dom b₃ holds
for b₄ being Real st b₄ < b₂ holds
ex b₅ being Real st
( b₄ < b₅ & b₅ < b₂ & b₅ in dom b₃ )

proof end;

theorem Th4: :: LIMFUNC2:4

for b₁, b₂ being Real
for b₃ being PartFunc of REAL , REAL st 0 < b₁ & ].b₂,(b₂ + b₁).[ c= dom b₃ holds
for b₄ being Real st b₂ < b₄ holds
ex b₅ being Real st
( b₅ < b₄ & b₂ < b₅ & b₅ in dom b₃ )

proof end;

theorem Th5: :: LIMFUNC2:5

for b₁ being Real
for b₂ being Real_Sequence
for b₃ being PartFunc of REAL , REAL st ( for b₄ being Nat holds
( b₁ - (1 / (b₄ + 1)) < b₂ . b₄ & b₂ . b₄ < b₁ & b₂ . b₄ in dom b₃ ) ) holds
( b₂ is convergent & lim b₂ = b₁ & rng b₂ c= dom b₃ & rng b₂ c= (dom b₃) /\ (left_open_halfline b₁) )

proof end;

theorem Th6: :: LIMFUNC2:6

for b₁ being Real
for b₂ being Real_Sequence
for b₃ being PartFunc of REAL , REAL st ( for b₄ being Nat holds
( b₁ < b₂ . b₄ & b₂ . b₄ < b₁ + (1 / (b₄ + 1)) & b₂ . b₄ in dom b₃ ) ) holds
( b₂ is convergent & lim b₂ = b₁ & rng b₂ c= dom b₃ & rng b₂ c= (dom b₃) /\ (right_open_halfline b₁) )

proof end;

definition

let c₁ be PartFunc of REAL , REAL ;
let c₂ be Real;
pred c₁ is_left_convergent_in c₂ means :Def1: :: LIMFUNC2:def 1
( ( for b₁ being Real st b₁ < a₂ holds
ex b₂ being Real st
( b₁ < b₂ & b₂ < a₂ & b₂ in dom a₁ ) ) & ex b₁ being Real st
for b₂ being Real_Sequence st b₂ is convergent & lim b₂ = a₂ & rng b₂ c= (dom a₁) /\ (left_open_halfline a₂) holds
( a₁ * b₂ is convergent & lim (a₁ * b₂) = b₁ ) );
pred c₁ is_left_divergent_to+infty_in c₂ means :Def2: :: LIMFUNC2:def 2
( ( for b₁ being Real st b₁ < a₂ holds
ex b₂ being Real st
( b₁ < b₂ & b₂ < a₂ & b₂ in dom a₁ ) ) & ( for b₁ being Real_Sequence st b₁ is convergent & lim b₁ = a₂ & rng b₁ c= (dom a₁) /\ (left_open_halfline a₂) holds
a₁ * b₁ is divergent_to+infty ) );
pred c₁ is_left_divergent_to-infty_in c₂ means :Def3: :: LIMFUNC2:def 3
( ( for b₁ being Real st b₁ < a₂ holds
ex b₂ being Real st
( b₁ < b₂ & b₂ < a₂ & b₂ in dom a₁ ) ) & ( for b₁ being Real_Sequence st b₁ is convergent & lim b₁ = a₂ & rng b₁ c= (dom a₁) /\ (left_open_halfline a₂) holds
a₁ * b₁ is divergent_to-infty ) );
pred c₁ is_right_convergent_in c₂ means :Def4: :: LIMFUNC2:def 4
( ( for b₁ being Real st a₂ < b₁ holds
ex b₂ being Real st
( b₂ < b₁ & a₂ < b₂ & b₂ in dom a₁ ) ) & ex b₁ being Real st
for b₂ being Real_Sequence st b₂ is convergent & lim b₂ = a₂ & rng b₂ c= (dom a₁) /\ (right_open_halfline a₂) holds
( a₁ * b₂ is convergent & lim (a₁ * b₂) = b₁ ) );
pred c₁ is_right_divergent_to+infty_in c₂ means :Def5: :: LIMFUNC2:def 5
( ( for b₁ being Real st a₂ < b₁ holds
ex b₂ being Real st
( b₂ < b₁ & a₂ < b₂ & b₂ in dom a₁ ) ) & ( for b₁ being Real_Sequence st b₁ is convergent & lim b₁ = a₂ & rng b₁ c= (dom a₁) /\ (right_open_halfline a₂) holds
a₁ * b₁ is divergent_to+infty ) );
pred c₁ is_right_divergent_to-infty_in c₂ means :Def6: :: LIMFUNC2:def 6
( ( for b₁ being Real st a₂ < b₁ holds
ex b₂ being Real st
( b₂ < b₁ & a₂ < b₂ & b₂ in dom a₁ ) ) & ( for b₁ being Real_Sequence st b₁ is convergent & lim b₁ = a₂ & rng b₁ c= (dom a₁) /\ (right_open_halfline a₂) holds
a₁ * b₁ is divergent_to-infty ) );

end;

:: deftheorem Def1 defines is_left_convergent_in LIMFUNC2:def 1 :

:: deftheorem Def2 defines is_left_divergent_to+infty_in LIMFUNC2:def 2 :

:: deftheorem Def3 defines is_left_divergent_to-infty_in LIMFUNC2:def 3 :

:: deftheorem Def4 defines is_right_convergent_in LIMFUNC2:def 4 :

:: deftheorem Def5 defines is_right_divergent_to+infty_in LIMFUNC2:def 5 :

:: deftheorem Def6 defines is_right_divergent_to-infty_in LIMFUNC2:def 6 :

theorem Th7: :: LIMFUNC2:7

canceled;

theorem Th8: :: LIMFUNC2:8

canceled;

theorem Th9: :: LIMFUNC2:9

canceled;

theorem Th10: :: LIMFUNC2:10

canceled;

theorem Th11: :: LIMFUNC2:11

canceled;

theorem Th12: :: LIMFUNC2:12

canceled;

theorem Th13: :: LIMFUNC2:13

for b₁ being Real
for b₂ being PartFunc of REAL , REAL holds
( b₂ is_left_convergent_in b₁ iff ( ( for b₃ being Real st b₃ < b₁ holds
ex b₄ being Real st
( b₃ < b₄ & b₄ < b₁ & b₄ in dom b₂ ) ) & ex b₃ being Real st
for b₄ being Real st 0 < b₄ holds
ex b₅ being Real st
( b₅ < b₁ & ( for b₆ being Real st b₅ < b₆ & b₆ < b₁ & b₆ in dom b₂ holds
abs ((b₂ . b₆) - b₃) < b₄ ) ) ) )

proof end;

theorem Th14: :: LIMFUNC2:14

for b₁ being Real
for b₂ being PartFunc of REAL , REAL holds
( b₂ is_left_divergent_to+infty_in b₁ iff ( ( for b₃ being Real st b₃ < b₁ holds
ex b₄ being Real st
( b₃ < b₄ & b₄ < b₁ & b₄ in dom b₂ ) ) & ( for b₃ being Real ex b₄ being Real st
( b₄ < b₁ & ( for b₅ being Real st b₄ < b₅ & b₅ < b₁ & b₅ in dom b₂ holds
b₃ < b₂ . b₅ ) ) ) ) )

proof end;

theorem Th15: :: LIMFUNC2:15

for b₁ being Real
for b₂ being PartFunc of REAL , REAL holds
( b₂ is_left_divergent_to-infty_in b₁ iff ( ( for b₃ being Real st b₃ < b₁ holds
ex b₄ being Real st
( b₃ < b₄ & b₄ < b₁ & b₄ in dom b₂ ) ) & ( for b₃ being Real ex b₄ being Real st
( b₄ < b₁ & ( for b₅ being Real st b₄ < b₅ & b₅ < b₁ & b₅ in dom b₂ holds
b₂ . b₅ < b₃ ) ) ) ) )

proof end;

theorem Th16: :: LIMFUNC2:16

for b₁ being Real
for b₂ being PartFunc of REAL , REAL holds
( b₂ is_right_convergent_in b₁ iff ( ( for b₃ being Real st b₁ < b₃ holds
ex b₄ being Real st
( b₄ < b₃ & b₁ < b₄ & b₄ in dom b₂ ) ) & ex b₃ being Real st
for b₄ being Real st 0 < b₄ holds
ex b₅ being Real st
( b₁ < b₅ & ( for b₆ being Real st b₆ < b₅ & b₁ < b₆ & b₆ in dom b₂ holds
abs ((b₂ . b₆) - b₃) < b₄ ) ) ) )

proof end;

theorem Th17: :: LIMFUNC2:17

for b₁ being Real
for b₂ being PartFunc of REAL , REAL holds
( b₂ is_right_divergent_to+infty_in b₁ iff ( ( for b₃ being Real st b₁ < b₃ holds
ex b₄ being Real st
( b₄ < b₃ & b₁ < b₄ & b₄ in dom b₂ ) ) & ( for b₃ being Real ex b₄ being Real st
( b₁ < b₄ & ( for b₅ being Real st b₅ < b₄ & b₁ < b₅ & b₅ in dom b₂ holds
b₃ < b₂ . b₅ ) ) ) ) )

proof end;

theorem Th18: :: LIMFUNC2:18

for b₁ being Real
for b₂ being PartFunc of REAL , REAL holds
( b₂ is_right_divergent_to-infty_in b₁ iff ( ( for b₃ being Real st b₁ < b₃ holds
ex b₄ being Real st
( b₄ < b₃ & b₁ < b₄ & b₄ in dom b₂ ) ) & ( for b₃ being Real ex b₄ being Real st
( b₁ < b₄ & ( for b₅ being Real st b₅ < b₄ & b₁ < b₅ & b₅ in dom b₂ holds
b₂ . b₅ < b₃ ) ) ) ) )

proof end;

theorem Th19: :: LIMFUNC2:19

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_left_divergent_to+infty_in b₁ & b₃ is_left_divergent_to+infty_in b₁ & ( for b₄ being Real st b₄ < b₁ holds
ex b₅ being Real st
( b₄ < b₅ & b₅ < b₁ & b₅ in (dom b₂) /\ (dom b₃) ) ) holds
( b₂ + b₃ is_left_divergent_to+infty_in b₁ & b₂ (#) b₃ is_left_divergent_to+infty_in b₁ )

proof end;

theorem Th20: :: LIMFUNC2:20

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_left_divergent_to-infty_in b₁ & b₃ is_left_divergent_to-infty_in b₁ & ( for b₄ being Real st b₄ < b₁ holds
ex b₅ being Real st
( b₄ < b₅ & b₅ < b₁ & b₅ in (dom b₂) /\ (dom b₃) ) ) holds
( b₂ + b₃ is_left_divergent_to-infty_in b₁ & b₂ (#) b₃ is_left_divergent_to+infty_in b₁ )

proof end;

theorem Th21: :: LIMFUNC2:21

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_right_divergent_to+infty_in b₁ & b₃ is_right_divergent_to+infty_in b₁ & ( for b₄ being Real st b₁ < b₄ holds
ex b₅ being Real st
( b₅ < b₄ & b₁ < b₅ & b₅ in (dom b₂) /\ (dom b₃) ) ) holds
( b₂ + b₃ is_right_divergent_to+infty_in b₁ & b₂ (#) b₃ is_right_divergent_to+infty_in b₁ )

proof end;

theorem Th22: :: LIMFUNC2:22

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_right_divergent_to-infty_in b₁ & b₃ is_right_divergent_to-infty_in b₁ & ( for b₄ being Real st b₁ < b₄ holds
ex b₅ being Real st
( b₅ < b₄ & b₁ < b₅ & b₅ in (dom b₂) /\ (dom b₃) ) ) holds
( b₂ + b₃ is_right_divergent_to-infty_in b₁ & b₂ (#) b₃ is_right_divergent_to+infty_in b₁ )

proof end;

theorem Th23: :: LIMFUNC2:23

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_left_divergent_to+infty_in b₁ & ( for b₄ being Real st b₄ < b₁ holds
ex b₅ being Real st
( b₄ < b₅ & b₅ < b₁ & b₅ in dom (b₂ + b₃) ) ) & ex b₄ being Real st
( 0 < b₄ & b₃ is_bounded_below_on ].(b₁ - b₄),b₁.[ ) holds
b₂ + b₃ is_left_divergent_to+infty_in b₁

proof end;

theorem Th24: :: LIMFUNC2:24

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_left_divergent_to+infty_in b₁ & ( for b₄ being Real st b₄ < b₁ holds
ex b₅ being Real st
( b₄ < b₅ & b₅ < b₁ & b₅ in dom (b₂ (#) b₃) ) ) & ex b₄, b₅ being Real st
( 0 < b₄ & 0 < b₅ & ( for b₆ being Real st b₆ in (dom b₃) /\ ].(b₁ - b₄),b₁.[ holds
b₅ <= b₃ . b₆ ) ) holds
b₂ (#) b₃ is_left_divergent_to+infty_in b₁

proof end;

theorem Th25: :: LIMFUNC2:25

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_right_divergent_to+infty_in b₁ & ( for b₄ being Real st b₁ < b₄ holds
ex b₅ being Real st
( b₅ < b₄ & b₁ < b₅ & b₅ in dom (b₂ + b₃) ) ) & ex b₄ being Real st
( 0 < b₄ & b₃ is_bounded_below_on ].b₁,(b₁ + b₄).[ ) holds
b₂ + b₃ is_right_divergent_to+infty_in b₁

proof end;

theorem Th26: :: LIMFUNC2:26

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_right_divergent_to+infty_in b₁ & ( for b₄ being Real st b₁ < b₄ holds
ex b₅ being Real st
( b₅ < b₄ & b₁ < b₅ & b₅ in dom (b₂ (#) b₃) ) ) & ex b₄, b₅ being Real st
( 0 < b₄ & 0 < b₅ & ( for b₆ being Real st b₆ in (dom b₃) /\ ].b₁,(b₁ + b₄).[ holds
b₅ <= b₃ . b₆ ) ) holds
b₂ (#) b₃ is_right_divergent_to+infty_in b₁

proof end;

theorem Th27: :: LIMFUNC2:27

proof end;

theorem Th28: :: LIMFUNC2:28

proof end;

theorem Th29: :: LIMFUNC2:29

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st ( b₂ is_left_divergent_to+infty_in b₁ or b₂ is_left_divergent_to-infty_in b₁ ) holds
abs b₂ is_left_divergent_to+infty_in b₁

proof end;

theorem Th30: :: LIMFUNC2:30

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st ( b₂ is_right_divergent_to+infty_in b₁ or b₂ is_right_divergent_to-infty_in b₁ ) holds
abs b₂ is_right_divergent_to+infty_in b₁

proof end;

theorem Th31: :: LIMFUNC2:31

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st ex b₃ being Real st
( 0 < b₃ & b₂ is_non_decreasing_on ].(b₁ - b₃),b₁.[ & not b₂ is_bounded_above_on ].(b₁ - b₃),b₁.[ ) & ( for b₃ being Real st b₃ < b₁ holds
ex b₄ being Real st
( b₃ < b₄ & b₄ < b₁ & b₄ in dom b₂ ) ) holds
b₂ is_left_divergent_to+infty_in b₁

proof end;

theorem Th32: :: LIMFUNC2:32

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st ex b₃ being Real st
( 0 < b₃ & b₂ is_increasing_on ].(b₁ - b₃),b₁.[ & not b₂ is_bounded_above_on ].(b₁ - b₃),b₁.[ ) & ( for b₃ being Real st b₃ < b₁ holds
ex b₄ being Real st
( b₃ < b₄ & b₄ < b₁ & b₄ in dom b₂ ) ) holds
b₂ is_left_divergent_to+infty_in b₁

proof end;

theorem Th33: :: LIMFUNC2:33

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st ex b₃ being Real st
( 0 < b₃ & b₂ is_non_increasing_on ].(b₁ - b₃),b₁.[ & not b₂ is_bounded_below_on ].(b₁ - b₃),b₁.[ ) & ( for b₃ being Real st b₃ < b₁ holds
ex b₄ being Real st
( b₃ < b₄ & b₄ < b₁ & b₄ in dom b₂ ) ) holds
b₂ is_left_divergent_to-infty_in b₁

proof end;

theorem Th34: :: LIMFUNC2:34

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st ex b₃ being Real st
( 0 < b₃ & b₂ is_decreasing_on ].(b₁ - b₃),b₁.[ & not b₂ is_bounded_below_on ].(b₁ - b₃),b₁.[ ) & ( for b₃ being Real st b₃ < b₁ holds
ex b₄ being Real st
( b₃ < b₄ & b₄ < b₁ & b₄ in dom b₂ ) ) holds
b₂ is_left_divergent_to-infty_in b₁

proof end;

theorem Th35: :: LIMFUNC2:35

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st ex b₃ being Real st
( 0 < b₃ & b₂ is_non_increasing_on ].b₁,(b₁ + b₃).[ & not b₂ is_bounded_above_on ].b₁,(b₁ + b₃).[ ) & ( for b₃ being Real st b₁ < b₃ holds
ex b₄ being Real st
( b₄ < b₃ & b₁ < b₄ & b₄ in dom b₂ ) ) holds
b₂ is_right_divergent_to+infty_in b₁

proof end;

theorem Th36: :: LIMFUNC2:36

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st ex b₃ being Real st
( 0 < b₃ & b₂ is_decreasing_on ].b₁,(b₁ + b₃).[ & not b₂ is_bounded_above_on ].b₁,(b₁ + b₃).[ ) & ( for b₃ being Real st b₁ < b₃ holds
ex b₄ being Real st
( b₄ < b₃ & b₁ < b₄ & b₄ in dom b₂ ) ) holds
b₂ is_right_divergent_to+infty_in b₁

proof end;

theorem Th37: :: LIMFUNC2:37

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st ex b₃ being Real st
( 0 < b₃ & b₂ is_non_decreasing_on ].b₁,(b₁ + b₃).[ & not b₂ is_bounded_below_on ].b₁,(b₁ + b₃).[ ) & ( for b₃ being Real st b₁ < b₃ holds
ex b₄ being Real st
( b₄ < b₃ & b₁ < b₄ & b₄ in dom b₂ ) ) holds
b₂ is_right_divergent_to-infty_in b₁

proof end;

theorem Th38: :: LIMFUNC2:38

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st ex b₃ being Real st
( 0 < b₃ & b₂ is_increasing_on ].b₁,(b₁ + b₃).[ & not b₂ is_bounded_below_on ].b₁,(b₁ + b₃).[ ) & ( for b₃ being Real st b₁ < b₃ holds
ex b₄ being Real st
( b₄ < b₃ & b₁ < b₄ & b₄ in dom b₂ ) ) holds
b₂ is_right_divergent_to-infty_in b₁

proof end;

theorem Th39: :: LIMFUNC2:39

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_left_divergent_to+infty_in b₁ & ( for b₄ being Real st b₄ < b₁ holds
ex b₅ being Real st
( b₄ < b₅ & b₅ < b₁ & b₅ in dom b₃ ) ) & ex b₄ being Real st
( 0 < b₄ & (dom b₃) /\ ].(b₁ - b₄),b₁.[ c= (dom b₂) /\ ].(b₁ - b₄),b₁.[ & ( for b₅ being Real st b₅ in (dom b₃) /\ ].(b₁ - b₄),b₁.[ holds
b₂ . b₅ <= b₃ . b₅ ) ) holds
b₃ is_left_divergent_to+infty_in b₁

proof end;

theorem Th40: :: LIMFUNC2:40

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_left_divergent_to-infty_in b₁ & ( for b₄ being Real st b₄ < b₁ holds
ex b₅ being Real st
( b₄ < b₅ & b₅ < b₁ & b₅ in dom b₃ ) ) & ex b₄ being Real st
( 0 < b₄ & (dom b₃) /\ ].(b₁ - b₄),b₁.[ c= (dom b₂) /\ ].(b₁ - b₄),b₁.[ & ( for b₅ being Real st b₅ in (dom b₃) /\ ].(b₁ - b₄),b₁.[ holds
b₃ . b₅ <= b₂ . b₅ ) ) holds
b₃ is_left_divergent_to-infty_in b₁

proof end;

theorem Th41: :: LIMFUNC2:41

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_right_divergent_to+infty_in b₁ & ( for b₄ being Real st b₁ < b₄ holds
ex b₅ being Real st
( b₅ < b₄ & b₁ < b₅ & b₅ in dom b₃ ) ) & ex b₄ being Real st
( 0 < b₄ & (dom b₃) /\ ].b₁,(b₁ + b₄).[ c= (dom b₂) /\ ].b₁,(b₁ + b₄).[ & ( for b₅ being Real st b₅ in (dom b₃) /\ ].b₁,(b₁ + b₄).[ holds
b₂ . b₅ <= b₃ . b₅ ) ) holds
b₃ is_right_divergent_to+infty_in b₁

proof end;

theorem Th42: :: LIMFUNC2:42

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_right_divergent_to-infty_in b₁ & ( for b₄ being Real st b₁ < b₄ holds
ex b₅ being Real st
( b₅ < b₄ & b₁ < b₅ & b₅ in dom b₃ ) ) & ex b₄ being Real st
( 0 < b₄ & (dom b₃) /\ ].b₁,(b₁ + b₄).[ c= (dom b₂) /\ ].b₁,(b₁ + b₄).[ & ( for b₅ being Real st b₅ in (dom b₃) /\ ].b₁,(b₁ + b₄).[ holds
b₃ . b₅ <= b₂ . b₅ ) ) holds
b₃ is_right_divergent_to-infty_in b₁

proof end;

theorem Th43: :: LIMFUNC2:43

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_left_divergent_to+infty_in b₁ & ex b₄ being Real st
( 0 < b₄ & ].(b₁ - b₄),b₁.[ c= (dom b₃) /\ (dom b₂) & ( for b₅ being Real st b₅ in ].(b₁ - b₄),b₁.[ holds
b₂ . b₅ <= b₃ . b₅ ) ) holds
b₃ is_left_divergent_to+infty_in b₁

proof end;

theorem Th44: :: LIMFUNC2:44

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_left_divergent_to-infty_in b₁ & ex b₄ being Real st
( 0 < b₄ & ].(b₁ - b₄),b₁.[ c= (dom b₃) /\ (dom b₂) & ( for b₅ being Real st b₅ in ].(b₁ - b₄),b₁.[ holds
b₃ . b₅ <= b₂ . b₅ ) ) holds
b₃ is_left_divergent_to-infty_in b₁

proof end;

theorem Th45: :: LIMFUNC2:45

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_right_divergent_to+infty_in b₁ & ex b₄ being Real st
( 0 < b₄ & ].b₁,(b₁ + b₄).[ c= (dom b₃) /\ (dom b₂) & ( for b₅ being Real st b₅ in ].b₁,(b₁ + b₄).[ holds
b₂ . b₅ <= b₃ . b₅ ) ) holds
b₃ is_right_divergent_to+infty_in b₁

proof end;

theorem Th46: :: LIMFUNC2:46

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_right_divergent_to-infty_in b₁ & ex b₄ being Real st
( 0 < b₄ & ].b₁,(b₁ + b₄).[ c= (dom b₃) /\ (dom b₂) & ( for b₅ being Real st b₅ in ].b₁,(b₁ + b₄).[ holds
b₃ . b₅ <= b₂ . b₅ ) ) holds
b₃ is_right_divergent_to-infty_in b₁

proof end;

definition

let c₁ be PartFunc of REAL , REAL ;
let c₂ be Real;
assume E26: c₁ is_left_convergent_in c₂ ;
func lim_left c₁,c₂ -> Real means :Def7: :: LIMFUNC2:def 7
for b₁ being Real_Sequence st b₁ is convergent & lim b₁ = a₂ & rng b₁ c= (dom a₁) /\ (left_open_halfline a₂) holds
( a₁ * b₁ is convergent & lim (a₁ * b₁) = a₃ );
existence by E26, Def1;
uniqueness

proof end;

end;

:: deftheorem Def7 defines lim_left LIMFUNC2:def 7 :

definition

let c₁ be PartFunc of REAL , REAL ;
let c₂ be Real;
assume E27: c₁ is_right_convergent_in c₂ ;
func lim_right c₁,c₂ -> Real means :Def8: :: LIMFUNC2:def 8
for b₁ being Real_Sequence st b₁ is convergent & lim b₁ = a₂ & rng b₁ c= (dom a₁) /\ (right_open_halfline a₂) holds
( a₁ * b₁ is convergent & lim (a₁ * b₁) = a₃ );
existence by E27, Def4;
uniqueness

proof end;

end;

:: deftheorem Def8 defines lim_right LIMFUNC2:def 8 :

theorem Th47: :: LIMFUNC2:47

canceled;

theorem Th48: :: LIMFUNC2:48

canceled;

theorem Th49: :: LIMFUNC2:49

for b₁, b₂ being Real
for b₃ being PartFunc of REAL , REAL st b₃ is_left_convergent_in b₁ holds
( lim_left b₃,b₁ = b₂ iff for b₄ being Real st 0 < b₄ holds
ex b₅ being Real st
( b₅ < b₁ & ( for b₆ being Real st b₅ < b₆ & b₆ < b₁ & b₆ in dom b₃ holds
abs ((b₃ . b₆) - b₂) < b₄ ) ) )

proof end;

theorem Th50: :: LIMFUNC2:50

for b₁, b₂ being Real
for b₃ being PartFunc of REAL , REAL st b₃ is_right_convergent_in b₁ holds
( lim_right b₃,b₁ = b₂ iff for b₄ being Real st 0 < b₄ holds
ex b₅ being Real st
( b₁ < b₅ & ( for b₆ being Real st b₆ < b₅ & b₁ < b₆ & b₆ in dom b₃ holds
abs ((b₃ . b₆) - b₂) < b₄ ) ) )

proof end;

theorem Th51: :: LIMFUNC2:51

for b₁, b₂ being Real
for b₃ being PartFunc of REAL , REAL st b₃ is_left_convergent_in b₁ holds
( b₂ (#) b₃ is_left_convergent_in b₁ & lim_left (b₂ (#) b₃),b₁ = b₂ * (lim_left b₃,b₁) )

proof end;

theorem Th52: :: LIMFUNC2:52

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ holds
( - b₂ is_left_convergent_in b₁ & lim_left (- b₂),b₁ = - (lim_left b₂,b₁) )

proof end;

theorem Th53: :: LIMFUNC2:53

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ & b₃ is_left_convergent_in b₁ & ( for b₄ being Real st b₄ < b₁ holds
ex b₅ being Real st
( b₄ < b₅ & b₅ < b₁ & b₅ in dom (b₂ + b₃) ) ) holds
( b₂ + b₃ is_left_convergent_in b₁ & lim_left (b₂ + b₃),b₁ = (lim_left b₂,b₁) + (lim_left b₃,b₁) )

proof end;

theorem Th54: :: LIMFUNC2:54

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ & b₃ is_left_convergent_in b₁ & ( for b₄ being Real st b₄ < b₁ holds
ex b₅ being Real st
( b₄ < b₅ & b₅ < b₁ & b₅ in dom (b₂ - b₃) ) ) holds
( b₂ - b₃ is_left_convergent_in b₁ & lim_left (b₂ - b₃),b₁ = (lim_left b₂,b₁) - (lim_left b₃,b₁) )

proof end;

theorem Th55: :: LIMFUNC2:55

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ & b₂ " {0} = {} & lim_left b₂,b₁ <> 0 holds
( b₂ ^ is_left_convergent_in b₁ & lim_left (b₂ ^ ),b₁ = (lim_left b₂,b₁) " )

proof end;

theorem Th56: :: LIMFUNC2:56

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ holds
( abs b₂ is_left_convergent_in b₁ & lim_left (abs b₂),b₁ = abs (lim_left b₂,b₁) )

proof end;

theorem Th57: :: LIMFUNC2:57

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ & lim_left b₂,b₁ <> 0 & ( for b₃ being Real st b₃ < b₁ holds
ex b₄ being Real st
( b₃ < b₄ & b₄ < b₁ & b₄ in dom b₂ & b₂ . b₄ <> 0 ) ) holds
( b₂ ^ is_left_convergent_in b₁ & lim_left (b₂ ^ ),b₁ = (lim_left b₂,b₁) " )

proof end;

theorem Th58: :: LIMFUNC2:58

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ & b₃ is_left_convergent_in b₁ & ( for b₄ being Real st b₄ < b₁ holds
ex b₅ being Real st
( b₄ < b₅ & b₅ < b₁ & b₅ in dom (b₂ (#) b₃) ) ) holds
( b₂ (#) b₃ is_left_convergent_in b₁ & lim_left (b₂ (#) b₃),b₁ = (lim_left b₂,b₁) * (lim_left b₃,b₁) )

proof end;

theorem Th59: :: LIMFUNC2:59

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ & b₃ is_left_convergent_in b₁ & lim_left b₃,b₁ <> 0 & ( for b₄ being Real st b₄ < b₁ holds
ex b₅ being Real st
( b₄ < b₅ & b₅ < b₁ & b₅ in dom (b₂ / b₃) ) ) holds
( b₂ / b₃ is_left_convergent_in b₁ & lim_left (b₂ / b₃),b₁ = (lim_left b₂,b₁) / (lim_left b₃,b₁) )

proof end;

theorem Th60: :: LIMFUNC2:60

for b₁, b₂ being Real
for b₃ being PartFunc of REAL , REAL st b₃ is_right_convergent_in b₁ holds
( b₂ (#) b₃ is_right_convergent_in b₁ & lim_right (b₂ (#) b₃),b₁ = b₂ * (lim_right b₃,b₁) )

proof end;

theorem Th61: :: LIMFUNC2:61

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ holds
( - b₂ is_right_convergent_in b₁ & lim_right (- b₂),b₁ = - (lim_right b₂,b₁) )

proof end;

theorem Th62: :: LIMFUNC2:62

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ & b₃ is_right_convergent_in b₁ & ( for b₄ being Real st b₁ < b₄ holds
ex b₅ being Real st
( b₅ < b₄ & b₁ < b₅ & b₅ in dom (b₂ + b₃) ) ) holds
( b₂ + b₃ is_right_convergent_in b₁ & lim_right (b₂ + b₃),b₁ = (lim_right b₂,b₁) + (lim_right b₃,b₁) )

proof end;

theorem Th63: :: LIMFUNC2:63

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ & b₃ is_right_convergent_in b₁ & ( for b₄ being Real st b₁ < b₄ holds
ex b₅ being Real st
( b₅ < b₄ & b₁ < b₅ & b₅ in dom (b₂ - b₃) ) ) holds
( b₂ - b₃ is_right_convergent_in b₁ & lim_right (b₂ - b₃),b₁ = (lim_right b₂,b₁) - (lim_right b₃,b₁) )

proof end;

theorem Th64: :: LIMFUNC2:64

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ & b₂ " {0} = {} & lim_right b₂,b₁ <> 0 holds
( b₂ ^ is_right_convergent_in b₁ & lim_right (b₂ ^ ),b₁ = (lim_right b₂,b₁) " )

proof end;

theorem Th65: :: LIMFUNC2:65

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ holds
( abs b₂ is_right_convergent_in b₁ & lim_right (abs b₂),b₁ = abs (lim_right b₂,b₁) )

proof end;

theorem Th66: :: LIMFUNC2:66

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ & lim_right b₂,b₁ <> 0 & ( for b₃ being Real st b₁ < b₃ holds
ex b₄ being Real st
( b₄ < b₃ & b₁ < b₄ & b₄ in dom b₂ & b₂ . b₄ <> 0 ) ) holds
( b₂ ^ is_right_convergent_in b₁ & lim_right (b₂ ^ ),b₁ = (lim_right b₂,b₁) " )

proof end;

theorem Th67: :: LIMFUNC2:67

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ & b₃ is_right_convergent_in b₁ & ( for b₄ being Real st b₁ < b₄ holds
ex b₅ being Real st
( b₅ < b₄ & b₁ < b₅ & b₅ in dom (b₂ (#) b₃) ) ) holds
( b₂ (#) b₃ is_right_convergent_in b₁ & lim_right (b₂ (#) b₃),b₁ = (lim_right b₂,b₁) * (lim_right b₃,b₁) )

proof end;

theorem Th68: :: LIMFUNC2:68

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ & b₃ is_right_convergent_in b₁ & lim_right b₃,b₁ <> 0 & ( for b₄ being Real st b₁ < b₄ holds
ex b₅ being Real st
( b₅ < b₄ & b₁ < b₅ & b₅ in dom (b₂ / b₃) ) ) holds
( b₂ / b₃ is_right_convergent_in b₁ & lim_right (b₂ / b₃),b₁ = (lim_right b₂,b₁) / (lim_right b₃,b₁) )

proof end;

theorem Th69: :: LIMFUNC2:69

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ & lim_left b₂,b₁ = 0 & ( for b₄ being Real st b₄ < b₁ holds
ex b₅ being Real st
( b₄ < b₅ & b₅ < b₁ & b₅ in dom (b₂ (#) b₃) ) ) & ex b₄ being Real st
( 0 < b₄ & b₃ is_bounded_on ].(b₁ - b₄),b₁.[ ) holds
( b₂ (#) b₃ is_left_convergent_in b₁ & lim_left (b₂ (#) b₃),b₁ = 0 )

proof end;

theorem Th70: :: LIMFUNC2:70

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ & lim_right b₂,b₁ = 0 & ( for b₄ being Real st b₁ < b₄ holds
ex b₅ being Real st
( b₅ < b₄ & b₁ < b₅ & b₅ in dom (b₂ (#) b₃) ) ) & ex b₄ being Real st
( 0 < b₄ & b₃ is_bounded_on ].b₁,(b₁ + b₄).[ ) holds
( b₂ (#) b₃ is_right_convergent_in b₁ & lim_right (b₂ (#) b₃),b₁ = 0 )

proof end;

theorem Th71: :: LIMFUNC2:71

for b₁ being Real
for b₂, b₃, b₄ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ & b₃ is_left_convergent_in b₁ & lim_left b₂,b₁ = lim_left b₃,b₁ & ( for b₅ being Real st b₅ < b₁ holds
ex b₆ being Real st
( b₅ < b₆ & b₆ < b₁ & b₆ in dom b₄ ) ) & ex b₅ being Real st
( 0 < b₅ & ( for b₆ being Real st b₆ in (dom b₄) /\ ].(b₁ - b₅),b₁.[ holds
( b₂ . b₆ <= b₄ . b₆ & b₄ . b₆ <= b₃ . b₆ ) ) & ( ( (dom b₂) /\ ].(b₁ - b₅),b₁.[ c= (dom b₃) /\ ].(b₁ - b₅),b₁.[ & (dom b₄) /\ ].(b₁ - b₅),b₁.[ c= (dom b₂) /\ ].(b₁ - b₅),b₁.[ ) or ( (dom b₃) /\ ].(b₁ - b₅),b₁.[ c= (dom b₂) /\ ].(b₁ - b₅),b₁.[ & (dom b₄) /\ ].(b₁ - b₅),b₁.[ c= (dom b₃) /\ ].(b₁ - b₅),b₁.[ ) ) ) holds
( b₄ is_left_convergent_in b₁ & lim_left b₄,b₁ = lim_left b₂,b₁ )

proof end;

theorem Th72: :: LIMFUNC2:72

for b₁ being Real
for b₂, b₃, b₄ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ & b₃ is_left_convergent_in b₁ & lim_left b₂,b₁ = lim_left b₃,b₁ & ex b₅ being Real st
( 0 < b₅ & ].(b₁ - b₅),b₁.[ c= ((dom b₂) /\ (dom b₃)) /\ (dom b₄) & ( for b₆ being Real st b₆ in ].(b₁ - b₅),b₁.[ holds
( b₂ . b₆ <= b₄ . b₆ & b₄ . b₆ <= b₃ . b₆ ) ) ) holds
( b₄ is_left_convergent_in b₁ & lim_left b₄,b₁ = lim_left b₂,b₁ )

proof end;

theorem Th73: :: LIMFUNC2:73

for b₁ being Real
for b₂, b₃, b₄ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ & b₃ is_right_convergent_in b₁ & lim_right b₂,b₁ = lim_right b₃,b₁ & ( for b₅ being Real st b₁ < b₅ holds
ex b₆ being Real st
( b₆ < b₅ & b₁ < b₆ & b₆ in dom b₄ ) ) & ex b₅ being Real st
( 0 < b₅ & ( for b₆ being Real st b₆ in (dom b₄) /\ ].b₁,(b₁ + b₅).[ holds
( b₂ . b₆ <= b₄ . b₆ & b₄ . b₆ <= b₃ . b₆ ) ) & ( ( (dom b₂) /\ ].b₁,(b₁ + b₅).[ c= (dom b₃) /\ ].b₁,(b₁ + b₅).[ & (dom b₄) /\ ].b₁,(b₁ + b₅).[ c= (dom b₂) /\ ].b₁,(b₁ + b₅).[ ) or ( (dom b₃) /\ ].b₁,(b₁ + b₅).[ c= (dom b₂) /\ ].b₁,(b₁ + b₅).[ & (dom b₄) /\ ].b₁,(b₁ + b₅).[ c= (dom b₃) /\ ].b₁,(b₁ + b₅).[ ) ) ) holds
( b₄ is_right_convergent_in b₁ & lim_right b₄,b₁ = lim_right b₂,b₁ )

proof end;

theorem Th74: :: LIMFUNC2:74

for b₁ being Real
for b₂, b₃, b₄ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ & b₃ is_right_convergent_in b₁ & lim_right b₂,b₁ = lim_right b₃,b₁ & ex b₅ being Real st
( 0 < b₅ & ].b₁,(b₁ + b₅).[ c= ((dom b₂) /\ (dom b₃)) /\ (dom b₄) & ( for b₆ being Real st b₆ in ].b₁,(b₁ + b₅).[ holds
( b₂ . b₆ <= b₄ . b₆ & b₄ . b₆ <= b₃ . b₆ ) ) ) holds
( b₄ is_right_convergent_in b₁ & lim_right b₄,b₁ = lim_right b₂,b₁ )

proof end;

theorem Th75: :: LIMFUNC2:75

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ & b₃ is_left_convergent_in b₁ & ex b₄ being Real st
( 0 < b₄ & ( ( (dom b₂) /\ ].(b₁ - b₄),b₁.[ c= (dom b₃) /\ ].(b₁ - b₄),b₁.[ & ( for b₅ being Real st b₅ in (dom b₂) /\ ].(b₁ - b₄),b₁.[ holds
b₂ . b₅ <= b₃ . b₅ ) ) or ( (dom b₃) /\ ].(b₁ - b₄),b₁.[ c= (dom b₂) /\ ].(b₁ - b₄),b₁.[ & ( for b₅ being Real st b₅ in (dom b₃) /\ ].(b₁ - b₄),b₁.[ holds
b₂ . b₅ <= b₃ . b₅ ) ) ) ) holds
lim_left b₂,b₁ <= lim_left b₃,b₁

proof end;

theorem Th76: :: LIMFUNC2:76

for b₁ being Real
for b₂, b₃ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ & b₃ is_right_convergent_in b₁ & ex b₄ being Real st
( 0 < b₄ & ( ( (dom b₂) /\ ].b₁,(b₁ + b₄).[ c= (dom b₃) /\ ].b₁,(b₁ + b₄).[ & ( for b₅ being Real st b₅ in (dom b₂) /\ ].b₁,(b₁ + b₄).[ holds
b₂ . b₅ <= b₃ . b₅ ) ) or ( (dom b₃) /\ ].b₁,(b₁ + b₄).[ c= (dom b₂) /\ ].b₁,(b₁ + b₄).[ & ( for b₅ being Real st b₅ in (dom b₃) /\ ].b₁,(b₁ + b₄).[ holds
b₂ . b₅ <= b₃ . b₅ ) ) ) ) holds
lim_right b₂,b₁ <= lim_right b₃,b₁

proof end;

theorem Th77: :: LIMFUNC2:77

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st ( b₂ is_left_divergent_to+infty_in b₁ or b₂ is_left_divergent_to-infty_in b₁ ) & ( for b₃ being Real st b₃ < b₁ holds
ex b₄ being Real st
( b₃ < b₄ & b₄ < b₁ & b₄ in dom b₂ & b₂ . b₄ <> 0 ) ) holds
( b₂ ^ is_left_convergent_in b₁ & lim_left (b₂ ^ ),b₁ = 0 )

proof end;

theorem Th78: :: LIMFUNC2:78

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st ( b₂ is_right_divergent_to+infty_in b₁ or b₂ is_right_divergent_to-infty_in b₁ ) & ( for b₃ being Real st b₁ < b₃ holds
ex b₄ being Real st
( b₄ < b₃ & b₁ < b₄ & b₄ in dom b₂ & b₂ . b₄ <> 0 ) ) holds
( b₂ ^ is_right_convergent_in b₁ & lim_right (b₂ ^ ),b₁ = 0 )

proof end;

theorem Th79: :: LIMFUNC2:79

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ & lim_left b₂,b₁ = 0 & ex b₃ being Real st
( 0 < b₃ & ( for b₄ being Real st b₄ in (dom b₂) /\ ].(b₁ - b₃),b₁.[ holds
0 < b₂ . b₄ ) ) holds
b₂ ^ is_left_divergent_to+infty_in b₁

proof end;

theorem Th80: :: LIMFUNC2:80

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ & lim_left b₂,b₁ = 0 & ex b₃ being Real st
( 0 < b₃ & ( for b₄ being Real st b₄ in (dom b₂) /\ ].(b₁ - b₃),b₁.[ holds
b₂ . b₄ < 0 ) ) holds
b₂ ^ is_left_divergent_to-infty_in b₁

proof end;

theorem Th81: :: LIMFUNC2:81

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ & lim_right b₂,b₁ = 0 & ex b₃ being Real st
( 0 < b₃ & ( for b₄ being Real st b₄ in (dom b₂) /\ ].b₁,(b₁ + b₃).[ holds
0 < b₂ . b₄ ) ) holds
b₂ ^ is_right_divergent_to+infty_in b₁

proof end;

theorem Th82: :: LIMFUNC2:82

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ & lim_right b₂,b₁ = 0 & ex b₃ being Real st
( 0 < b₃ & ( for b₄ being Real st b₄ in (dom b₂) /\ ].b₁,(b₁ + b₃).[ holds
b₂ . b₄ < 0 ) ) holds
b₂ ^ is_right_divergent_to-infty_in b₁

proof end;

theorem Th83: :: LIMFUNC2:83

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ & lim_left b₂,b₁ = 0 & ( for b₃ being Real st b₃ < b₁ holds
ex b₄ being Real st
( b₃ < b₄ & b₄ < b₁ & b₄ in dom b₂ & b₂ . b₄ <> 0 ) ) & ex b₃ being Real st
( 0 < b₃ & ( for b₄ being Real st b₄ in (dom b₂) /\ ].(b₁ - b₃),b₁.[ holds
0 <= b₂ . b₄ ) ) holds
b₂ ^ is_left_divergent_to+infty_in b₁

proof end;

theorem Th84: :: LIMFUNC2:84

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_left_convergent_in b₁ & lim_left b₂,b₁ = 0 & ( for b₃ being Real st b₃ < b₁ holds
ex b₄ being Real st
( b₃ < b₄ & b₄ < b₁ & b₄ in dom b₂ & b₂ . b₄ <> 0 ) ) & ex b₃ being Real st
( 0 < b₃ & ( for b₄ being Real st b₄ in (dom b₂) /\ ].(b₁ - b₃),b₁.[ holds
b₂ . b₄ <= 0 ) ) holds
b₂ ^ is_left_divergent_to-infty_in b₁

proof end;

theorem Th85: :: LIMFUNC2:85

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ & lim_right b₂,b₁ = 0 & ( for b₃ being Real st b₁ < b₃ holds
ex b₄ being Real st
( b₄ < b₃ & b₁ < b₄ & b₄ in dom b₂ & b₂ . b₄ <> 0 ) ) & ex b₃ being Real st
( 0 < b₃ & ( for b₄ being Real st b₄ in (dom b₂) /\ ].b₁,(b₁ + b₃).[ holds
0 <= b₂ . b₄ ) ) holds
b₂ ^ is_right_divergent_to+infty_in b₁

proof end;

theorem Th86: :: LIMFUNC2:86

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_right_convergent_in b₁ & lim_right b₂,b₁ = 0 & ( for b₃ being Real st b₁ < b₃ holds
ex b₄ being Real st
( b₄ < b₃ & b₁ < b₄ & b₄ in dom b₂ & b₂ . b₄ <> 0 ) ) & ex b₃ being Real st
( 0 < b₃ & ( for b₄ being Real st b₄ in (dom b₂) /\ ].b₁,(b₁ + b₃).[ holds
b₂ . b₄ <= 0 ) ) holds
b₂ ^ is_right_divergent_to-infty_in b₁

proof end;