:: LIMFUNC1 semantic presentation

Lemma1: (- 1) * (- 1) = 1
;

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

proof end;

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

proof end;

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

proof end;

definition

let c₁, c₂ be Nat;
redefine func max as max c₁,c₂ -> Nat;
coherence by FINSEQ_2:1;

end;

Lemma5: for b₁, b₂, b₃, b₄ being real number st 0 <= b₁ & b₁ < b₂ & 0 < b₃ & b₃ <= b₄ holds
b₁ * b₃ < b₂ * b₄
by XREAL_1:99;

notation

let c₁ be real number ;
synonym left_open_halfline c₁ for halfline c₁;

end;

definition

let c₁ be real number ;
func left_closed_halfline c₁ -> Subset of REAL equals :: LIMFUNC1:def 1
{ b₁ where B is Real : b₁ <= a₁ } ;
coherence

proof end;

func right_closed_halfline c₁ -> Subset of REAL equals :: LIMFUNC1:def 2
{ b₁ where B is Real : a₁ <= b₁ } ;
coherence

proof end;

func right_open_halfline c₁ -> Subset of REAL equals :: LIMFUNC1:def 3
{ b₁ where B is Real : a₁ < b₁ } ;
coherence

proof end;

end;

:: deftheorem Def1 defines left_closed_halfline LIMFUNC1:def 1 :

:: deftheorem Def2 defines right_closed_halfline LIMFUNC1:def 2 :

:: deftheorem Def3 defines right_open_halfline LIMFUNC1:def 3 :

theorem Th1: :: LIMFUNC1:1

canceled;

theorem Th2: :: LIMFUNC1:2

canceled;

theorem Th3: :: LIMFUNC1:3

canceled;

theorem Th4: :: LIMFUNC1:4

canceled;

theorem Th5: :: LIMFUNC1:5

canceled;

theorem Th6: :: LIMFUNC1:6

canceled;

theorem Th7: :: LIMFUNC1:7

canceled;

theorem Th8: :: LIMFUNC1:8

for b₁, b₂ being real number st b₁ <= b₂ holds
right_open_halfline b₂ c= right_open_halfline b₁

proof end;

theorem Th9: :: LIMFUNC1:9

for b₁, b₂ being real number st b₁ <= b₂ holds
right_closed_halfline b₂ c= right_closed_halfline b₁

proof end;

theorem Th10: :: LIMFUNC1:10

for b₁ being real number holds right_open_halfline b₁ c= right_closed_halfline b₁

proof end;

theorem Th11: :: LIMFUNC1:11

for b₁, b₂ being real number holds ].b₁,b₂.[ c= right_open_halfline b₁

proof end;

theorem Th12: :: LIMFUNC1:12

for b₁, b₂ being real number holds [.b₁,b₂.] c= right_closed_halfline b₁

proof end;

theorem Th13: :: LIMFUNC1:13

for b₁, b₂ being real number st b₁ <= b₂ holds
left_open_halfline b₁ c= left_open_halfline b₂

proof end;

theorem Th14: :: LIMFUNC1:14

for b₁, b₂ being real number st b₁ <= b₂ holds
left_closed_halfline b₁ c= left_closed_halfline b₂

proof end;

theorem Th15: :: LIMFUNC1:15

for b₁ being real number holds left_open_halfline b₁ c= left_closed_halfline b₁

proof end;

theorem Th16: :: LIMFUNC1:16

for b₁, b₂ being real number holds ].b₁,b₂.[ c= left_open_halfline b₂

proof end;

theorem Th17: :: LIMFUNC1:17

for b₁, b₂ being real number holds [.b₁,b₂.] c= left_closed_halfline b₂

proof end;

theorem Th18: :: LIMFUNC1:18

for b₁, b₂ being real number holds (left_open_halfline b₁) /\ (right_open_halfline b₂) = ].b₂,b₁.[

proof end;

theorem Th19: :: LIMFUNC1:19

for b₁, b₂ being real number holds (left_closed_halfline b₁) /\ (right_closed_halfline b₂) = [.b₂,b₁.]

proof end;

theorem Th20: :: LIMFUNC1:20

for b₁, b₂, b₃ being real number st b₁ <= b₂ holds
( ].b₂,b₃.[ c= right_open_halfline b₁ & [.b₂,b₃.] c= right_closed_halfline b₁ )

proof end;

theorem Th21: :: LIMFUNC1:21

for b₁, b₂, b₃ being real number st b₁ < b₂ holds
[.b₂,b₃.] c= right_open_halfline b₁

proof end;

theorem Th22: :: LIMFUNC1:22

for b₁, b₂, b₃ being real number st b₁ <= b₂ holds
( ].b₃,b₁.[ c= left_open_halfline b₂ & [.b₃,b₁.] c= left_closed_halfline b₂ )

proof end;

theorem Th23: :: LIMFUNC1:23

for b₁, b₂, b₃ being real number st b₁ < b₂ holds
[.b₃,b₁.] c= left_open_halfline b₂

proof end;

theorem Th24: :: LIMFUNC1:24

for b₁ being real number holds
( REAL \ (right_open_halfline b₁) = left_closed_halfline b₁ & REAL \ (right_closed_halfline b₁) = left_open_halfline b₁ & REAL \ (left_open_halfline b₁) = right_closed_halfline b₁ & REAL \ (left_closed_halfline b₁) = right_open_halfline b₁ )

proof end;

theorem Th25: :: LIMFUNC1:25

for b₁, b₂ being real number holds
( REAL \ ].b₁,b₂.[ = (left_closed_halfline b₁) \/ (right_closed_halfline b₂) & REAL \ [.b₁,b₂.] = (left_open_halfline b₁) \/ (right_open_halfline b₂) )

proof end;

theorem Th26: :: LIMFUNC1:26

for b₁ being Real_Sequence holds
( ( b₁ is non-decreasing implies b₁ is bounded_below ) & ( b₁ is non-increasing implies b₁ is bounded_above ) )

proof end;

theorem Th27: :: LIMFUNC1:27

for b₁ being Real_Sequence st b₁ is_not_0 & b₁ is convergent & lim b₁ = 0 & b₁ is non-decreasing holds
for b₂ being Nat holds b₁ . b₂ < 0

proof end;

theorem Th28: :: LIMFUNC1:28

for b₁ being Real_Sequence st b₁ is_not_0 & b₁ is convergent & lim b₁ = 0 & b₁ is non-increasing holds
for b₂ being Nat holds 0 < b₁ . b₂

proof end;

theorem Th29: :: LIMFUNC1:29

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

proof end;

theorem Th30: :: LIMFUNC1:30

for b₁ being Real_Sequence st b₁ is convergent & 0 < lim b₁ holds
ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
(lim b₁) / 2 < b₁ . b₃

proof end;

definition

let c₁ be Real_Sequence;
attr a₁ is divergent_to+infty means :Def4: :: LIMFUNC1:def 4
for b₁ being Real ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
b₁ < a₁ . b₃;
attr a₁ is divergent_to-infty means :Def5: :: LIMFUNC1:def 5
for b₁ being Real ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
a₁ . b₃ < b₁;

end;

:: deftheorem Def4 defines divergent_to+infty LIMFUNC1:def 4 :

:: deftheorem Def5 defines divergent_to-infty LIMFUNC1:def 5 :

theorem Th31: :: LIMFUNC1:31

canceled;

theorem Th32: :: LIMFUNC1:32

canceled;

theorem Th33: :: LIMFUNC1:33

for b₁ being Real_Sequence st ( b₁ is divergent_to+infty or b₁ is divergent_to-infty ) holds
ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
b₁ ^\ b₃ is_not_0

proof end;

theorem Th34: :: LIMFUNC1:34

for b₁ being Nat
for b₂ being Real_Sequence holds
( ( b₂ ^\ b₁ is divergent_to+infty implies b₂ is divergent_to+infty ) & ( b₂ ^\ b₁ is divergent_to-infty implies b₂ is divergent_to-infty ) )

proof end;

theorem Th35: :: LIMFUNC1:35

for b₁, b₂ being Real_Sequence st b₁ is divergent_to+infty & b₂ is divergent_to+infty holds
b₁ + b₂ is divergent_to+infty

proof end;

theorem Th36: :: LIMFUNC1:36

for b₁, b₂ being Real_Sequence st b₁ is divergent_to+infty & b₂ is bounded_below holds
b₁ + b₂ is divergent_to+infty

proof end;

theorem Th37: :: LIMFUNC1:37

for b₁, b₂ being Real_Sequence st b₁ is divergent_to+infty & b₂ is divergent_to+infty holds
b₁ (#) b₂ is divergent_to+infty

proof end;

theorem Th38: :: LIMFUNC1:38

for b₁, b₂ being Real_Sequence st b₁ is divergent_to-infty & b₂ is divergent_to-infty holds
b₁ + b₂ is divergent_to-infty

proof end;

theorem Th39: :: LIMFUNC1:39

for b₁, b₂ being Real_Sequence st b₁ is divergent_to-infty & b₂ is bounded_above holds
b₁ + b₂ is divergent_to-infty

proof end;

theorem Th40: :: LIMFUNC1:40

for b₁ being Real_Sequence
for b₂ being Real holds
( ( b₁ is divergent_to+infty & b₂ > 0 implies b₂ (#) b₁ is divergent_to+infty ) & ( b₁ is divergent_to+infty & b₂ < 0 implies b₂ (#) b₁ is divergent_to-infty ) & ( b₁ is divergent_to+infty & b₂ = 0 implies ( rng (b₂ (#) b₁) = {0} & b₂ (#) b₁ is constant ) ) )

proof end;

theorem Th41: :: LIMFUNC1:41

for b₁ being Real_Sequence
for b₂ being Real holds
( ( b₁ is divergent_to-infty & b₂ > 0 implies b₂ (#) b₁ is divergent_to-infty ) & ( b₁ is divergent_to-infty & b₂ < 0 implies b₂ (#) b₁ is divergent_to+infty ) & ( b₁ is divergent_to-infty & b₂ = 0 implies ( rng (b₂ (#) b₁) = {0} & b₂ (#) b₁ is constant ) ) )

proof end;

theorem Th42: :: LIMFUNC1:42

for b₁ being Real_Sequence holds
( ( b₁ is divergent_to+infty implies - b₁ is divergent_to-infty ) & ( b₁ is divergent_to-infty implies - b₁ is divergent_to+infty ) )

proof end;

theorem Th43: :: LIMFUNC1:43

for b₁, b₂ being Real_Sequence st b₁ is bounded_below & b₂ is divergent_to-infty holds
b₁ - b₂ is divergent_to+infty

proof end;

theorem Th44: :: LIMFUNC1:44

for b₁, b₂ being Real_Sequence st b₁ is bounded_above & b₂ is divergent_to+infty holds
b₁ - b₂ is divergent_to-infty

proof end;

theorem Th45: :: LIMFUNC1:45

for b₁, b₂ being Real_Sequence st b₁ is divergent_to+infty & b₂ is convergent holds
b₁ + b₂ is divergent_to+infty

proof end;

theorem Th46: :: LIMFUNC1:46

for b₁, b₂ being Real_Sequence st b₁ is divergent_to-infty & b₂ is convergent holds
b₁ + b₂ is divergent_to-infty

proof end;

theorem Th47: :: LIMFUNC1:47

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = b₂ ) holds
b₁ is divergent_to+infty

proof end;

set c₁ = incl NAT ;

Lemma25: for b₁ being Nat holds (incl NAT ) . b₁ = b₁
by FUNCT_1:35;

theorem Th48: :: LIMFUNC1:48

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = - b₂ ) holds
b₁ is divergent_to-infty

proof end;

theorem Th49: :: LIMFUNC1:49

for b₁, b₂ being Real_Sequence st b₁ is divergent_to+infty & ex b₃ being Real st
( b₃ > 0 & ( for b₄ being Nat holds b₂ . b₄ >= b₃ ) ) holds
b₁ (#) b₂ is divergent_to+infty

proof end;

theorem Th50: :: LIMFUNC1:50

for b₁, b₂ being Real_Sequence st b₁ is divergent_to-infty & ex b₃ being Real st
( 0 < b₃ & ( for b₄ being Nat holds b₂ . b₄ >= b₃ ) ) holds
b₁ (#) b₂ is divergent_to-infty

proof end;

theorem Th51: :: LIMFUNC1:51

for b₁, b₂ being Real_Sequence st b₁ is divergent_to-infty & b₂ is divergent_to-infty holds
b₁ (#) b₂ is divergent_to+infty

proof end;

theorem Th52: :: LIMFUNC1:52

for b₁ being Real_Sequence st ( b₁ is divergent_to+infty or b₁ is divergent_to-infty ) holds
abs b₁ is divergent_to+infty

proof end;

theorem Th53: :: LIMFUNC1:53

for b₁, b₂ being Real_Sequence st b₁ is divergent_to+infty & b₂ is subsequence of b₁ holds
b₂ is divergent_to+infty

proof end;

theorem Th54: :: LIMFUNC1:54

for b₁, b₂ being Real_Sequence st b₁ is divergent_to-infty & b₂ is subsequence of b₁ holds
b₂ is divergent_to-infty

proof end;

theorem Th55: :: LIMFUNC1:55

for b₁, b₂ being Real_Sequence st b₁ is divergent_to+infty & b₂ is convergent & 0 < lim b₂ holds
b₁ (#) b₂ is divergent_to+infty

proof end;

theorem Th56: :: LIMFUNC1:56

for b₁ being Real_Sequence st b₁ is non-decreasing & not b₁ is bounded_above holds
b₁ is divergent_to+infty

proof end;

theorem Th57: :: LIMFUNC1:57

for b₁ being Real_Sequence st b₁ is non-increasing & not b₁ is bounded_below holds
b₁ is divergent_to-infty

proof end;

theorem Th58: :: LIMFUNC1:58

for b₁ being Real_Sequence st b₁ is increasing & not b₁ is bounded_above holds
b₁ is divergent_to+infty

proof end;

theorem Th59: :: LIMFUNC1:59

for b₁ being Real_Sequence st b₁ is decreasing & not b₁ is bounded_below holds
b₁ is divergent_to-infty

proof end;

theorem Th60: :: LIMFUNC1:60

for b₁ being Real_Sequence holds
( not b₁ is monotone or b₁ is convergent or b₁ is divergent_to+infty or b₁ is divergent_to-infty )

proof end;

theorem Th61: :: LIMFUNC1:61

for b₁ being Real_Sequence st ( b₁ is divergent_to+infty or b₁ is divergent_to-infty ) holds
( b₁ " is convergent & lim (b₁ " ) = 0 )

proof end;

theorem Th62: :: LIMFUNC1:62

for b₁ being Real_Sequence st b₁ is_not_0 & b₁ is convergent & lim b₁ = 0 & ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
0 < b₁ . b₃ holds
b₁ " is divergent_to+infty

proof end;

theorem Th63: :: LIMFUNC1:63

for b₁ being Real_Sequence st b₁ is_not_0 & b₁ is convergent & lim b₁ = 0 & ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
b₁ . b₃ < 0 holds
b₁ " is divergent_to-infty

proof end;

theorem Th64: :: LIMFUNC1:64

for b₁ being Real_Sequence st b₁ is_not_0 & b₁ is convergent & lim b₁ = 0 & b₁ is non-decreasing holds
b₁ " is divergent_to-infty

proof end;

theorem Th65: :: LIMFUNC1:65

for b₁ being Real_Sequence st b₁ is_not_0 & b₁ is convergent & lim b₁ = 0 & b₁ is non-increasing holds
b₁ " is divergent_to+infty

proof end;

theorem Th66: :: LIMFUNC1:66

for b₁ being Real_Sequence st b₁ is_not_0 & b₁ is convergent & lim b₁ = 0 & b₁ is increasing holds
b₁ " is divergent_to-infty

proof end;

theorem Th67: :: LIMFUNC1:67

for b₁ being Real_Sequence st b₁ is_not_0 & b₁ is convergent & lim b₁ = 0 & b₁ is decreasing holds
b₁ " is divergent_to+infty

proof end;

theorem Th68: :: LIMFUNC1:68

for b₁, b₂ being Real_Sequence st b₁ is bounded & ( b₂ is divergent_to+infty or b₂ is divergent_to-infty ) & b₂ is_not_0 holds
( b₁ /" b₂ is convergent & lim (b₁ /" b₂) = 0 )

proof end;

theorem Th69: :: LIMFUNC1:69

for b₁, b₂ being Real_Sequence st b₁ is divergent_to+infty & ( for b₃ being Nat holds b₁ . b₃ <= b₂ . b₃ ) holds
b₂ is divergent_to+infty

proof end;

theorem Th70: :: LIMFUNC1:70

for b₁, b₂ being Real_Sequence st b₁ is divergent_to-infty & ( for b₃ being Nat holds b₂ . b₃ <= b₁ . b₃ ) holds
b₂ is divergent_to-infty

proof end;

definition

let c₂ be PartFunc of REAL , REAL ;
attr a₁ is convergent_in+infty means :Def6: :: LIMFUNC1:def 6
( ( for b₁ being Real ex b₂ being Real st
( b₁ < b₂ & b₂ in dom a₁ ) ) & ex b₁ being Real st
for b₂ being Real_Sequence st b₂ is divergent_to+infty & rng b₂ c= dom a₁ holds
( a₁ * b₂ is convergent & lim (a₁ * b₂) = b₁ ) );
attr a₁ is divergent_in+infty_to+infty means :Def7: :: LIMFUNC1:def 7
( ( for b₁ being Real ex b₂ being Real st
( b₁ < b₂ & b₂ in dom a₁ ) ) & ( for b₁ being Real_Sequence st b₁ is divergent_to+infty & rng b₁ c= dom a₁ holds
a₁ * b₁ is divergent_to+infty ) );
attr a₁ is divergent_in+infty_to-infty means :Def8: :: LIMFUNC1:def 8
( ( for b₁ being Real ex b₂ being Real st
( b₁ < b₂ & b₂ in dom a₁ ) ) & ( for b₁ being Real_Sequence st b₁ is divergent_to+infty & rng b₁ c= dom a₁ holds
a₁ * b₁ is divergent_to-infty ) );
attr a₁ is convergent_in-infty means :Def9: :: LIMFUNC1:def 9
( ( for b₁ being Real ex b₂ being Real st
( b₂ < b₁ & b₂ in dom a₁ ) ) & ex b₁ being Real st
for b₂ being Real_Sequence st b₂ is divergent_to-infty & rng b₂ c= dom a₁ holds
( a₁ * b₂ is convergent & lim (a₁ * b₂) = b₁ ) );
attr a₁ is divergent_in-infty_to+infty means :Def10: :: LIMFUNC1:def 10
( ( for b₁ being Real ex b₂ being Real st
( b₂ < b₁ & b₂ in dom a₁ ) ) & ( for b₁ being Real_Sequence st b₁ is divergent_to-infty & rng b₁ c= dom a₁ holds
a₁ * b₁ is divergent_to+infty ) );
attr a₁ is divergent_in-infty_to-infty means :Def11: :: LIMFUNC1:def 11
( ( for b₁ being Real ex b₂ being Real st
( b₂ < b₁ & b₂ in dom a₁ ) ) & ( for b₁ being Real_Sequence st b₁ is divergent_to-infty & rng b₁ c= dom a₁ holds
a₁ * b₁ is divergent_to-infty ) );

end;

:: deftheorem Def6 defines convergent_in+infty LIMFUNC1:def 6 :

:: deftheorem Def7 defines divergent_in+infty_to+infty LIMFUNC1:def 7 :

:: deftheorem Def8 defines divergent_in+infty_to-infty LIMFUNC1:def 8 :

:: deftheorem Def9 defines convergent_in-infty LIMFUNC1:def 9 :

:: deftheorem Def10 defines divergent_in-infty_to+infty LIMFUNC1:def 10 :

:: deftheorem Def11 defines divergent_in-infty_to-infty LIMFUNC1:def 11 :

theorem Th71: :: LIMFUNC1:71

canceled;

theorem Th72: :: LIMFUNC1:72

canceled;

theorem Th73: :: LIMFUNC1:73

canceled;

theorem Th74: :: LIMFUNC1:74

canceled;

theorem Th75: :: LIMFUNC1:75

canceled;

theorem Th76: :: LIMFUNC1:76

canceled;

theorem Th77: :: LIMFUNC1:77

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

proof end;

theorem Th78: :: LIMFUNC1:78

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

proof end;

theorem Th79: :: LIMFUNC1:79

for b₁ being PartFunc of REAL , REAL holds
( b₁ is divergent_in+infty_to+infty iff ( ( for b₂ being Real ex b₃ being Real st
( b₂ < b₃ & b₃ in dom b₁ ) ) & ( for b₂ being Real ex b₃ being Real st
for b₄ being Real st b₃ < b₄ & b₄ in dom b₁ holds
b₂ < b₁ . b₄ ) ) )

proof end;

theorem Th80: :: LIMFUNC1:80

for b₁ being PartFunc of REAL , REAL holds
( b₁ is divergent_in+infty_to-infty iff ( ( for b₂ being Real ex b₃ being Real st
( b₂ < b₃ & b₃ in dom b₁ ) ) & ( for b₂ being Real ex b₃ being Real st
for b₄ being Real st b₃ < b₄ & b₄ in dom b₁ holds
b₁ . b₄ < b₂ ) ) )

proof end;

theorem Th81: :: LIMFUNC1:81

for b₁ being PartFunc of REAL , REAL holds
( b₁ is divergent_in-infty_to+infty iff ( ( for b₂ being Real ex b₃ being Real st
( b₃ < b₂ & b₃ in dom b₁ ) ) & ( for b₂ being Real ex b₃ being Real st
for b₄ being Real st b₄ < b₃ & b₄ in dom b₁ holds
b₂ < b₁ . b₄ ) ) )

proof end;

theorem Th82: :: LIMFUNC1:82

for b₁ being PartFunc of REAL , REAL holds
( b₁ is divergent_in-infty_to-infty iff ( ( for b₂ being Real ex b₃ being Real st
( b₃ < b₂ & b₃ in dom b₁ ) ) & ( for b₂ being Real ex b₃ being Real st
for b₄ being Real st b₄ < b₃ & b₄ in dom b₁ holds
b₁ . b₄ < b₂ ) ) )

proof end;

theorem Th83: :: LIMFUNC1:83

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in+infty_to+infty & b₂ is divergent_in+infty_to+infty & ( for b₃ being Real ex b₄ being Real st
( b₃ < b₄ & b₄ in (dom b₁) /\ (dom b₂) ) ) holds
( b₁ + b₂ is divergent_in+infty_to+infty & b₁ (#) b₂ is divergent_in+infty_to+infty )

proof end;

theorem Th84: :: LIMFUNC1:84

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in+infty_to-infty & b₂ is divergent_in+infty_to-infty & ( for b₃ being Real ex b₄ being Real st
( b₃ < b₄ & b₄ in (dom b₁) /\ (dom b₂) ) ) holds
( b₁ + b₂ is divergent_in+infty_to-infty & b₁ (#) b₂ is divergent_in+infty_to+infty )

proof end;

theorem Th85: :: LIMFUNC1:85

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in-infty_to+infty & b₂ is divergent_in-infty_to+infty & ( for b₃ being Real ex b₄ being Real st
( b₄ < b₃ & b₄ in (dom b₁) /\ (dom b₂) ) ) holds
( b₁ + b₂ is divergent_in-infty_to+infty & b₁ (#) b₂ is divergent_in-infty_to+infty )

proof end;

theorem Th86: :: LIMFUNC1:86

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in-infty_to-infty & b₂ is divergent_in-infty_to-infty & ( for b₃ being Real ex b₄ being Real st
( b₄ < b₃ & b₄ in (dom b₁) /\ (dom b₂) ) ) holds
( b₁ + b₂ is divergent_in-infty_to-infty & b₁ (#) b₂ is divergent_in-infty_to+infty )

proof end;

theorem Th87: :: LIMFUNC1:87

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in+infty_to+infty & ( for b₃ being Real ex b₄ being Real st
( b₃ < b₄ & b₄ in dom (b₁ + b₂) ) ) & ex b₃ being Real st b₂ is_bounded_below_on right_open_halfline b₃ holds
b₁ + b₂ is divergent_in+infty_to+infty

proof end;

theorem Th88: :: LIMFUNC1:88

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in+infty_to+infty & ( for b₃ being Real ex b₄ being Real st
( b₃ < b₄ & b₄ in dom (b₁ (#) b₂) ) ) & ex b₃, b₄ being Real st
( 0 < b₃ & ( for b₅ being Real st b₅ in (dom b₂) /\ (right_open_halfline b₄) holds
b₃ <= b₂ . b₅ ) ) holds
b₁ (#) b₂ is divergent_in+infty_to+infty

proof end;

theorem Th89: :: LIMFUNC1:89

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in-infty_to+infty & ( for b₃ being Real ex b₄ being Real st
( b₄ < b₃ & b₄ in dom (b₁ + b₂) ) ) & ex b₃ being Real st b₂ is_bounded_below_on left_open_halfline b₃ holds
b₁ + b₂ is divergent_in-infty_to+infty

proof end;

theorem Th90: :: LIMFUNC1:90

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in-infty_to+infty & ( for b₃ being Real ex b₄ being Real st
( b₄ < b₃ & b₄ in dom (b₁ (#) b₂) ) ) & ex b₃, b₄ being Real st
( 0 < b₃ & ( for b₅ being Real st b₅ in (dom b₂) /\ (left_open_halfline b₄) holds
b₃ <= b₂ . b₅ ) ) holds
b₁ (#) b₂ is divergent_in-infty_to+infty

proof end;

theorem Th91: :: LIMFUNC1:91

for b₁ being PartFunc of REAL , REAL
for b₂ being Real holds
( ( b₁ is divergent_in+infty_to+infty & b₂ > 0 implies b₂ (#) b₁ is divergent_in+infty_to+infty ) & ( b₁ is divergent_in+infty_to+infty & b₂ < 0 implies b₂ (#) b₁ is divergent_in+infty_to-infty ) & ( b₁ is divergent_in+infty_to-infty & b₂ > 0 implies b₂ (#) b₁ is divergent_in+infty_to-infty ) & ( b₁ is divergent_in+infty_to-infty & b₂ < 0 implies b₂ (#) b₁ is divergent_in+infty_to+infty ) )

proof end;

theorem Th92: :: LIMFUNC1:92

for b₁ being PartFunc of REAL , REAL
for b₂ being Real holds
( ( b₁ is divergent_in-infty_to+infty & b₂ > 0 implies b₂ (#) b₁ is divergent_in-infty_to+infty ) & ( b₁ is divergent_in-infty_to+infty & b₂ < 0 implies b₂ (#) b₁ is divergent_in-infty_to-infty ) & ( b₁ is divergent_in-infty_to-infty & b₂ > 0 implies b₂ (#) b₁ is divergent_in-infty_to-infty ) & ( b₁ is divergent_in-infty_to-infty & b₂ < 0 implies b₂ (#) b₁ is divergent_in-infty_to+infty ) )

proof end;

theorem Th93: :: LIMFUNC1:93

for b₁ being PartFunc of REAL , REAL st ( b₁ is divergent_in+infty_to+infty or b₁ is divergent_in+infty_to-infty ) holds
abs b₁ is divergent_in+infty_to+infty

proof end;

theorem Th94: :: LIMFUNC1:94

for b₁ being PartFunc of REAL , REAL st ( b₁ is divergent_in-infty_to+infty or b₁ is divergent_in-infty_to-infty ) holds
abs b₁ is divergent_in-infty_to+infty

proof end;

theorem Th95: :: LIMFUNC1:95

for b₁ being PartFunc of REAL , REAL st ex b₂ being Real st
( b₁ is_non_decreasing_on right_open_halfline b₂ & not b₁ is_bounded_above_on right_open_halfline b₂ ) & ( for b₂ being Real ex b₃ being Real st
( b₂ < b₃ & b₃ in dom b₁ ) ) holds
b₁ is divergent_in+infty_to+infty

proof end;

theorem Th96: :: LIMFUNC1:96

for b₁ being PartFunc of REAL , REAL st ex b₂ being Real st
( b₁ is_increasing_on right_open_halfline b₂ & not b₁ is_bounded_above_on right_open_halfline b₂ ) & ( for b₂ being Real ex b₃ being Real st
( b₂ < b₃ & b₃ in dom b₁ ) ) holds
b₁ is divergent_in+infty_to+infty

proof end;

theorem Th97: :: LIMFUNC1:97

for b₁ being PartFunc of REAL , REAL st ex b₂ being Real st
( b₁ is_non_increasing_on right_open_halfline b₂ & not b₁ is_bounded_below_on right_open_halfline b₂ ) & ( for b₂ being Real ex b₃ being Real st
( b₂ < b₃ & b₃ in dom b₁ ) ) holds
b₁ is divergent_in+infty_to-infty

proof end;

theorem Th98: :: LIMFUNC1:98

for b₁ being PartFunc of REAL , REAL st ex b₂ being Real st
( b₁ is_decreasing_on right_open_halfline b₂ & not b₁ is_bounded_below_on right_open_halfline b₂ ) & ( for b₂ being Real ex b₃ being Real st
( b₂ < b₃ & b₃ in dom b₁ ) ) holds
b₁ is divergent_in+infty_to-infty

proof end;

theorem Th99: :: LIMFUNC1:99

for b₁ being PartFunc of REAL , REAL st ex b₂ being Real st
( b₁ is_non_increasing_on left_open_halfline b₂ & not b₁ is_bounded_above_on left_open_halfline b₂ ) & ( for b₂ being Real ex b₃ being Real st
( b₃ < b₂ & b₃ in dom b₁ ) ) holds
b₁ is divergent_in-infty_to+infty

proof end;

theorem Th100: :: LIMFUNC1:100

for b₁ being PartFunc of REAL , REAL st ex b₂ being Real st
( b₁ is_decreasing_on left_open_halfline b₂ & not b₁ is_bounded_above_on left_open_halfline b₂ ) & ( for b₂ being Real ex b₃ being Real st
( b₃ < b₂ & b₃ in dom b₁ ) ) holds
b₁ is divergent_in-infty_to+infty

proof end;

theorem Th101: :: LIMFUNC1:101

for b₁ being PartFunc of REAL , REAL st ex b₂ being Real st
( b₁ is_non_decreasing_on left_open_halfline b₂ & not b₁ is_bounded_below_on left_open_halfline b₂ ) & ( for b₂ being Real ex b₃ being Real st
( b₃ < b₂ & b₃ in dom b₁ ) ) holds
b₁ is divergent_in-infty_to-infty

proof end;

theorem Th102: :: LIMFUNC1:102

for b₁ being PartFunc of REAL , REAL st ex b₂ being Real st
( b₁ is_increasing_on left_open_halfline b₂ & not b₁ is_bounded_below_on left_open_halfline b₂ ) & ( for b₂ being Real ex b₃ being Real st
( b₃ < b₂ & b₃ in dom b₁ ) ) holds
b₁ is divergent_in-infty_to-infty

proof end;

theorem Th103: :: LIMFUNC1:103

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in+infty_to+infty & ( for b₃ being Real ex b₄ being Real st
( b₃ < b₄ & b₄ in dom b₂ ) ) & ex b₃ being Real st
( (dom b₂) /\ (right_open_halfline b₃) c= (dom b₁) /\ (right_open_halfline b₃) & ( for b₄ being Real st b₄ in (dom b₂) /\ (right_open_halfline b₃) holds
b₁ . b₄ <= b₂ . b₄ ) ) holds
b₂ is divergent_in+infty_to+infty

proof end;

theorem Th104: :: LIMFUNC1:104

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in+infty_to-infty & ( for b₃ being Real ex b₄ being Real st
( b₃ < b₄ & b₄ in dom b₂ ) ) & ex b₃ being Real st
( (dom b₂) /\ (right_open_halfline b₃) c= (dom b₁) /\ (right_open_halfline b₃) & ( for b₄ being Real st b₄ in (dom b₂) /\ (right_open_halfline b₃) holds
b₂ . b₄ <= b₁ . b₄ ) ) holds
b₂ is divergent_in+infty_to-infty

proof end;

theorem Th105: :: LIMFUNC1:105

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in-infty_to+infty & ( for b₃ being Real ex b₄ being Real st
( b₄ < b₃ & b₄ in dom b₂ ) ) & ex b₃ being Real st
( (dom b₂) /\ (left_open_halfline b₃) c= (dom b₁) /\ (left_open_halfline b₃) & ( for b₄ being Real st b₄ in (dom b₂) /\ (left_open_halfline b₃) holds
b₁ . b₄ <= b₂ . b₄ ) ) holds
b₂ is divergent_in-infty_to+infty

proof end;

theorem Th106: :: LIMFUNC1:106

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in-infty_to-infty & ( for b₃ being Real ex b₄ being Real st
( b₄ < b₃ & b₄ in dom b₂ ) ) & ex b₃ being Real st
( (dom b₂) /\ (left_open_halfline b₃) c= (dom b₁) /\ (left_open_halfline b₃) & ( for b₄ being Real st b₄ in (dom b₂) /\ (left_open_halfline b₃) holds
b₂ . b₄ <= b₁ . b₄ ) ) holds
b₂ is divergent_in-infty_to-infty

proof end;

theorem Th107: :: LIMFUNC1:107

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in+infty_to+infty & ex b₃ being Real st
( right_open_halfline b₃ c= (dom b₂) /\ (dom b₁) & ( for b₄ being Real st b₄ in right_open_halfline b₃ holds
b₁ . b₄ <= b₂ . b₄ ) ) holds
b₂ is divergent_in+infty_to+infty

proof end;

theorem Th108: :: LIMFUNC1:108

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in+infty_to-infty & ex b₃ being Real st
( right_open_halfline b₃ c= (dom b₂) /\ (dom b₁) & ( for b₄ being Real st b₄ in right_open_halfline b₃ holds
b₂ . b₄ <= b₁ . b₄ ) ) holds
b₂ is divergent_in+infty_to-infty

proof end;

theorem Th109: :: LIMFUNC1:109

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in-infty_to+infty & ex b₃ being Real st
( left_open_halfline b₃ c= (dom b₂) /\ (dom b₁) & ( for b₄ being Real st b₄ in left_open_halfline b₃ holds
b₁ . b₄ <= b₂ . b₄ ) ) holds
b₂ is divergent_in-infty_to+infty

proof end;

theorem Th110: :: LIMFUNC1:110

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is divergent_in-infty_to-infty & ex b₃ being Real st
( left_open_halfline b₃ c= (dom b₂) /\ (dom b₁) & ( for b₄ being Real st b₄ in left_open_halfline b₃ holds
b₂ . b₄ <= b₁ . b₄ ) ) holds
b₂ is divergent_in-infty_to-infty

proof end;

definition

let c₂ be PartFunc of REAL , REAL ;
assume E55: c₂ is convergent_in+infty ;
func lim_in+infty c₁ -> Real means :Def12: :: LIMFUNC1:def 12
for b₁ being Real_Sequence st b₁ is divergent_to+infty & rng b₁ c= dom a₁ holds
( a₁ * b₁ is convergent & lim (a₁ * b₁) = a₂ );
existence by E55, Def6;
uniqueness

proof end;

end;

:: deftheorem Def12 defines lim_in+infty LIMFUNC1:def 12 :

definition

let c₂ be PartFunc of REAL , REAL ;
assume E56: c₂ is convergent_in-infty ;
func lim_in-infty c₁ -> Real means :Def13: :: LIMFUNC1:def 13
for b₁ being Real_Sequence st b₁ is divergent_to-infty & rng b₁ c= dom a₁ holds
( a₁ * b₁ is convergent & lim (a₁ * b₁) = a₂ );
existence by E56, Def9;
uniqueness

proof end;

end;

:: deftheorem Def13 defines lim_in-infty LIMFUNC1:def 13 :

theorem Th111: :: LIMFUNC1:111

canceled;

theorem Th112: :: LIMFUNC1:112

canceled;

theorem Th113: :: LIMFUNC1:113

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

proof end;

theorem Th114: :: LIMFUNC1:114

for b₁ being PartFunc of REAL , REAL
for b₂ being Real st b₁ is convergent_in+infty holds
( lim_in+infty b₁ = b₂ iff for b₃ being Real st 0 < b₃ holds
ex b₄ being Real st
for b₅ being Real st b₄ < b₅ & b₅ in dom b₁ holds
abs ((b₁ . b₅) - b₂) < b₃ )

proof end;

theorem Th115: :: LIMFUNC1:115

for b₁ being PartFunc of REAL , REAL
for b₂ being Real st b₁ is convergent_in+infty holds
( b₂ (#) b₁ is convergent_in+infty & lim_in+infty (b₂ (#) b₁) = b₂ * (lim_in+infty b₁) )

proof end;

theorem Th116: :: LIMFUNC1:116

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in+infty holds
( - b₁ is convergent_in+infty & lim_in+infty (- b₁) = - (lim_in+infty b₁) )

proof end;

theorem Th117: :: LIMFUNC1:117

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is convergent_in+infty & b₂ is convergent_in+infty & ( for b₃ being Real ex b₄ being Real st
( b₃ < b₄ & b₄ in dom (b₁ + b₂) ) ) holds
( b₁ + b₂ is convergent_in+infty & lim_in+infty (b₁ + b₂) = (lim_in+infty b₁) + (lim_in+infty b₂) )

proof end;

theorem Th118: :: LIMFUNC1:118

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is convergent_in+infty & b₂ is convergent_in+infty & ( for b₃ being Real ex b₄ being Real st
( b₃ < b₄ & b₄ in dom (b₁ - b₂) ) ) holds
( b₁ - b₂ is convergent_in+infty & lim_in+infty (b₁ - b₂) = (lim_in+infty b₁) - (lim_in+infty b₂) )

proof end;

theorem Th119: :: LIMFUNC1:119

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in+infty & b₁ " {0} = {} & lim_in+infty b₁ <> 0 holds
( b₁ ^ is convergent_in+infty & lim_in+infty (b₁ ^ ) = (lim_in+infty b₁) " )

proof end;

theorem Th120: :: LIMFUNC1:120

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in+infty holds
( abs b₁ is convergent_in+infty & lim_in+infty (abs b₁) = abs (lim_in+infty b₁) )

proof end;

theorem Th121: :: LIMFUNC1:121

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in+infty & lim_in+infty b₁ <> 0 & ( for b₂ being Real ex b₃ being Real st
( b₂ < b₃ & b₃ in dom b₁ & b₁ . b₃ <> 0 ) ) holds
( b₁ ^ is convergent_in+infty & lim_in+infty (b₁ ^ ) = (lim_in+infty b₁) " )

proof end;

theorem Th122: :: LIMFUNC1:122

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is convergent_in+infty & b₂ is convergent_in+infty & ( for b₃ being Real ex b₄ being Real st
( b₃ < b₄ & b₄ in dom (b₁ (#) b₂) ) ) holds
( b₁ (#) b₂ is convergent_in+infty & lim_in+infty (b₁ (#) b₂) = (lim_in+infty b₁) * (lim_in+infty b₂) )

proof end;

theorem Th123: :: LIMFUNC1:123

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is convergent_in+infty & b₂ is convergent_in+infty & lim_in+infty b₂ <> 0 & ( for b₃ being Real ex b₄ being Real st
( b₃ < b₄ & b₄ in dom (b₁ / b₂) ) ) holds
( b₁ / b₂ is convergent_in+infty & lim_in+infty (b₁ / b₂) = (lim_in+infty b₁) / (lim_in+infty b₂) )

proof end;

theorem Th124: :: LIMFUNC1:124

for b₁ being PartFunc of REAL , REAL
for b₂ being Real st b₁ is convergent_in-infty holds
( b₂ (#) b₁ is convergent_in-infty & lim_in-infty (b₂ (#) b₁) = b₂ * (lim_in-infty b₁) )

proof end;

theorem Th125: :: LIMFUNC1:125

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in-infty holds
( - b₁ is convergent_in-infty & lim_in-infty (- b₁) = - (lim_in-infty b₁) )

proof end;

theorem Th126: :: LIMFUNC1:126

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is convergent_in-infty & b₂ is convergent_in-infty & ( for b₃ being Real ex b₄ being Real st
( b₄ < b₃ & b₄ in dom (b₁ + b₂) ) ) holds
( b₁ + b₂ is convergent_in-infty & lim_in-infty (b₁ + b₂) = (lim_in-infty b₁) + (lim_in-infty b₂) )

proof end;

theorem Th127: :: LIMFUNC1:127

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is convergent_in-infty & b₂ is convergent_in-infty & ( for b₃ being Real ex b₄ being Real st
( b₄ < b₃ & b₄ in dom (b₁ - b₂) ) ) holds
( b₁ - b₂ is convergent_in-infty & lim_in-infty (b₁ - b₂) = (lim_in-infty b₁) - (lim_in-infty b₂) )

proof end;

theorem Th128: :: LIMFUNC1:128

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in-infty & b₁ " {0} = {} & lim_in-infty b₁ <> 0 holds
( b₁ ^ is convergent_in-infty & lim_in-infty (b₁ ^ ) = (lim_in-infty b₁) " )

proof end;

theorem Th129: :: LIMFUNC1:129

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in-infty holds
( abs b₁ is convergent_in-infty & lim_in-infty (abs b₁) = abs (lim_in-infty b₁) )

proof end;

theorem Th130: :: LIMFUNC1:130

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in-infty & lim_in-infty b₁ <> 0 & ( for b₂ being Real ex b₃ being Real st
( b₃ < b₂ & b₃ in dom b₁ & b₁ . b₃ <> 0 ) ) holds
( b₁ ^ is convergent_in-infty & lim_in-infty (b₁ ^ ) = (lim_in-infty b₁) " )

proof end;

theorem Th131: :: LIMFUNC1:131

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is convergent_in-infty & b₂ is convergent_in-infty & ( for b₃ being Real ex b₄ being Real st
( b₄ < b₃ & b₄ in dom (b₁ (#) b₂) ) ) holds
( b₁ (#) b₂ is convergent_in-infty & lim_in-infty (b₁ (#) b₂) = (lim_in-infty b₁) * (lim_in-infty b₂) )

proof end;

theorem Th132: :: LIMFUNC1:132

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is convergent_in-infty & b₂ is convergent_in-infty & lim_in-infty b₂ <> 0 & ( for b₃ being Real ex b₄ being Real st
( b₄ < b₃ & b₄ in dom (b₁ / b₂) ) ) holds
( b₁ / b₂ is convergent_in-infty & lim_in-infty (b₁ / b₂) = (lim_in-infty b₁) / (lim_in-infty b₂) )

proof end;

theorem Th133: :: LIMFUNC1:133

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is convergent_in+infty & lim_in+infty b₁ = 0 & ( for b₃ being Real ex b₄ being Real st
( b₃ < b₄ & b₄ in dom (b₁ (#) b₂) ) ) & ex b₃ being Real st b₂ is_bounded_on right_open_halfline b₃ holds
( b₁ (#) b₂ is convergent_in+infty & lim_in+infty (b₁ (#) b₂) = 0 )

proof end;

theorem Th134: :: LIMFUNC1:134

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is convergent_in-infty & lim_in-infty b₁ = 0 & ( for b₃ being Real ex b₄ being Real st
( b₄ < b₃ & b₄ in dom (b₁ (#) b₂) ) ) & ex b₃ being Real st b₂ is_bounded_on left_open_halfline b₃ holds
( b₁ (#) b₂ is convergent_in-infty & lim_in-infty (b₁ (#) b₂) = 0 )

proof end;

theorem Th135: :: LIMFUNC1:135

for b₁, b₂, b₃ being PartFunc of REAL , REAL st b₁ is convergent_in+infty & b₂ is convergent_in+infty & lim_in+infty b₁ = lim_in+infty b₂ & ( for b₄ being Real ex b₅ being Real st
( b₄ < b₅ & b₅ in dom b₃ ) ) & ex b₄ being Real st
( ( ( (dom b₁) /\ (right_open_halfline b₄) c= (dom b₂) /\ (right_open_halfline b₄) & (dom b₃) /\ (right_open_halfline b₄) c= (dom b₁) /\ (right_open_halfline b₄) ) or ( (dom b₂) /\ (right_open_halfline b₄) c= (dom b₁) /\ (right_open_halfline b₄) & (dom b₃) /\ (right_open_halfline b₄) c= (dom b₂) /\ (right_open_halfline b₄) ) ) & ( for b₅ being Real st b₅ in (dom b₃) /\ (right_open_halfline b₄) holds
( b₁ . b₅ <= b₃ . b₅ & b₃ . b₅ <= b₂ . b₅ ) ) ) holds
( b₃ is convergent_in+infty & lim_in+infty b₃ = lim_in+infty b₁ )

proof end;

theorem Th136: :: LIMFUNC1:136

for b₁, b₂, b₃ being PartFunc of REAL , REAL st b₁ is convergent_in+infty & b₂ is convergent_in+infty & lim_in+infty b₁ = lim_in+infty b₂ & ex b₄ being Real st
( right_open_halfline b₄ c= ((dom b₁) /\ (dom b₂)) /\ (dom b₃) & ( for b₅ being Real st b₅ in right_open_halfline b₄ holds
( b₁ . b₅ <= b₃ . b₅ & b₃ . b₅ <= b₂ . b₅ ) ) ) holds
( b₃ is convergent_in+infty & lim_in+infty b₃ = lim_in+infty b₁ )

proof end;

theorem Th137: :: LIMFUNC1:137

for b₁, b₂, b₃ being PartFunc of REAL , REAL st b₁ is convergent_in-infty & b₂ is convergent_in-infty & lim_in-infty b₁ = lim_in-infty b₂ & ( for b₄ being Real ex b₅ being Real st
( b₅ < b₄ & b₅ in dom b₃ ) ) & ex b₄ being Real st
( ( ( (dom b₁) /\ (left_open_halfline b₄) c= (dom b₂) /\ (left_open_halfline b₄) & (dom b₃) /\ (left_open_halfline b₄) c= (dom b₁) /\ (left_open_halfline b₄) ) or ( (dom b₂) /\ (left_open_halfline b₄) c= (dom b₁) /\ (left_open_halfline b₄) & (dom b₃) /\ (left_open_halfline b₄) c= (dom b₂) /\ (left_open_halfline b₄) ) ) & ( for b₅ being Real st b₅ in (dom b₃) /\ (left_open_halfline b₄) holds
( b₁ . b₅ <= b₃ . b₅ & b₃ . b₅ <= b₂ . b₅ ) ) ) holds
( b₃ is convergent_in-infty & lim_in-infty b₃ = lim_in-infty b₁ )

proof end;

theorem Th138: :: LIMFUNC1:138

for b₁, b₂, b₃ being PartFunc of REAL , REAL st b₁ is convergent_in-infty & b₂ is convergent_in-infty & lim_in-infty b₁ = lim_in-infty b₂ & ex b₄ being Real st
( left_open_halfline b₄ c= ((dom b₁) /\ (dom b₂)) /\ (dom b₃) & ( for b₅ being Real st b₅ in left_open_halfline b₄ holds
( b₁ . b₅ <= b₃ . b₅ & b₃ . b₅ <= b₂ . b₅ ) ) ) holds
( b₃ is convergent_in-infty & lim_in-infty b₃ = lim_in-infty b₁ )

proof end;

theorem Th139: :: LIMFUNC1:139

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is convergent_in+infty & b₂ is convergent_in+infty & ex b₃ being Real st
( ( (dom b₁) /\ (right_open_halfline b₃) c= (dom b₂) /\ (right_open_halfline b₃) & ( for b₄ being Real st b₄ in (dom b₁) /\ (right_open_halfline b₃) holds
b₁ . b₄ <= b₂ . b₄ ) ) or ( (dom b₂) /\ (right_open_halfline b₃) c= (dom b₁) /\ (right_open_halfline b₃) & ( for b₄ being Real st b₄ in (dom b₂) /\ (right_open_halfline b₃) holds
b₁ . b₄ <= b₂ . b₄ ) ) ) holds
lim_in+infty b₁ <= lim_in+infty b₂

proof end;

theorem Th140: :: LIMFUNC1:140

for b₁, b₂ being PartFunc of REAL , REAL st b₁ is convergent_in-infty & b₂ is convergent_in-infty & ex b₃ being Real st
( ( (dom b₁) /\ (left_open_halfline b₃) c= (dom b₂) /\ (left_open_halfline b₃) & ( for b₄ being Real st b₄ in (dom b₁) /\ (left_open_halfline b₃) holds
b₁ . b₄ <= b₂ . b₄ ) ) or ( (dom b₂) /\ (left_open_halfline b₃) c= (dom b₁) /\ (left_open_halfline b₃) & ( for b₄ being Real st b₄ in (dom b₂) /\ (left_open_halfline b₃) holds
b₁ . b₄ <= b₂ . b₄ ) ) ) holds
lim_in-infty b₁ <= lim_in-infty b₂

proof end;

theorem Th141: :: LIMFUNC1:141

for b₁ being PartFunc of REAL , REAL st ( b₁ is divergent_in+infty_to+infty or b₁ is divergent_in+infty_to-infty ) & ( for b₂ being Real ex b₃ being Real st
( b₂ < b₃ & b₃ in dom b₁ & b₁ . b₃ <> 0 ) ) holds
( b₁ ^ is convergent_in+infty & lim_in+infty (b₁ ^ ) = 0 )

proof end;

theorem Th142: :: LIMFUNC1:142

for b₁ being PartFunc of REAL , REAL st ( b₁ is divergent_in-infty_to+infty or b₁ is divergent_in-infty_to-infty ) & ( for b₂ being Real ex b₃ being Real st
( b₃ < b₂ & b₃ in dom b₁ & b₁ . b₃ <> 0 ) ) holds
( b₁ ^ is convergent_in-infty & lim_in-infty (b₁ ^ ) = 0 )

proof end;

theorem Th143: :: LIMFUNC1:143

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in+infty & lim_in+infty b₁ = 0 & ( for b₂ being Real ex b₃ being Real st
( b₂ < b₃ & b₃ in dom b₁ & b₁ . b₃ <> 0 ) ) & ex b₂ being Real st
for b₃ being Real st b₃ in (dom b₁) /\ (right_open_halfline b₂) holds
0 <= b₁ . b₃ holds
b₁ ^ is divergent_in+infty_to+infty

proof end;

theorem Th144: :: LIMFUNC1:144

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in+infty & lim_in+infty b₁ = 0 & ( for b₂ being Real ex b₃ being Real st
( b₂ < b₃ & b₃ in dom b₁ & b₁ . b₃ <> 0 ) ) & ex b₂ being Real st
for b₃ being Real st b₃ in (dom b₁) /\ (right_open_halfline b₂) holds
b₁ . b₃ <= 0 holds
b₁ ^ is divergent_in+infty_to-infty

proof end;

theorem Th145: :: LIMFUNC1:145

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in-infty & lim_in-infty b₁ = 0 & ( for b₂ being Real ex b₃ being Real st
( b₃ < b₂ & b₃ in dom b₁ & b₁ . b₃ <> 0 ) ) & ex b₂ being Real st
for b₃ being Real st b₃ in (dom b₁) /\ (left_open_halfline b₂) holds
0 <= b₁ . b₃ holds
b₁ ^ is divergent_in-infty_to+infty

proof end;

theorem Th146: :: LIMFUNC1:146

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in-infty & lim_in-infty b₁ = 0 & ( for b₂ being Real ex b₃ being Real st
( b₃ < b₂ & b₃ in dom b₁ & b₁ . b₃ <> 0 ) ) & ex b₂ being Real st
for b₃ being Real st b₃ in (dom b₁) /\ (left_open_halfline b₂) holds
b₁ . b₃ <= 0 holds
b₁ ^ is divergent_in-infty_to-infty

proof end;

theorem Th147: :: LIMFUNC1:147

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in+infty & lim_in+infty b₁ = 0 & ex b₂ being Real st
for b₃ being Real st b₃ in (dom b₁) /\ (right_open_halfline b₂) holds
0 < b₁ . b₃ holds
b₁ ^ is divergent_in+infty_to+infty

proof end;

theorem Th148: :: LIMFUNC1:148

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in+infty & lim_in+infty b₁ = 0 & ex b₂ being Real st
for b₃ being Real st b₃ in (dom b₁) /\ (right_open_halfline b₂) holds
b₁ . b₃ < 0 holds
b₁ ^ is divergent_in+infty_to-infty

proof end;

theorem Th149: :: LIMFUNC1:149

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in-infty & lim_in-infty b₁ = 0 & ex b₂ being Real st
for b₃ being Real st b₃ in (dom b₁) /\ (left_open_halfline b₂) holds
0 < b₁ . b₃ holds
b₁ ^ is divergent_in-infty_to+infty

proof end;

theorem Th150: :: LIMFUNC1:150

for b₁ being PartFunc of REAL , REAL st b₁ is convergent_in-infty & lim_in-infty b₁ = 0 & ex b₂ being Real st
for b₃ being Real st b₃ in (dom b₁) /\ (left_open_halfline b₂) holds
b₁ . b₃ < 0 holds
b₁ ^ is divergent_in-infty_to-infty

proof end;