:: The Limit of a Real Function at Infinity. Halflines. Real Sequence Divergent to Infinity
:: by Jaros{\l}aw Kotowicz
::
:: Received August 20, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users


begin

Lm1: for g, r, r1 being real number st 0 < g & r <= r1 holds
( r - g < r1 & r < r1 + g )
proof end;

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

Lm3: for seq being Real_Sequence
for f1, f2 being PartFunc of REAL,REAL st rng seq c= dom (f1 (#) f2) holds
( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 )
proof end;

definition
let n, m be Element of NAT ;
:: original: max
redefine func max (n,m) -> Element of NAT ;
coherence
max (n,m) is Element of NAT by FINSEQ_2:1;
end;

notation
let r be real number ;
synonym left_open_halfline r for halfline r;
end;

definition
let r be real number ;
func left_closed_halfline r -> Subset of REAL equals :: LIMFUNC1:def 1
].-infty,r.];
coherence
].-infty,r.] is Subset of REAL
proof end;
func right_closed_halfline r -> Subset of REAL equals :: LIMFUNC1:def 2
[.r,+infty.[;
coherence
[.r,+infty.[ is Subset of REAL
proof end;
func right_open_halfline r -> Subset of REAL equals :: LIMFUNC1:def 3
].r,+infty.[;
coherence
].r,+infty.[ is Subset of REAL
proof end;
end;

:: deftheorem defines left_closed_halfline LIMFUNC1:def 1 :
for r being real number holds left_closed_halfline r = ].-infty,r.];

:: deftheorem defines right_closed_halfline LIMFUNC1:def 2 :
for r being real number holds right_closed_halfline r = [.r,+infty.[;

:: deftheorem defines right_open_halfline LIMFUNC1:def 3 :
for r being real number holds right_open_halfline r = ].r,+infty.[;

theorem :: LIMFUNC1:1
canceled;

theorem :: LIMFUNC1:2
canceled;

theorem :: LIMFUNC1:3
canceled;

theorem :: LIMFUNC1:4
canceled;

theorem :: LIMFUNC1:5
canceled;

theorem :: LIMFUNC1:6
canceled;

theorem :: LIMFUNC1:7
canceled;

theorem :: LIMFUNC1:8
canceled;

theorem :: LIMFUNC1:9
canceled;

theorem :: LIMFUNC1:10
canceled;

theorem :: LIMFUNC1:11
canceled;

theorem :: LIMFUNC1:12
canceled;

theorem :: LIMFUNC1:13
canceled;

theorem :: LIMFUNC1:14
canceled;

theorem :: LIMFUNC1:15
canceled;

theorem :: LIMFUNC1:16
canceled;

theorem :: LIMFUNC1:17
canceled;

theorem :: LIMFUNC1:18
canceled;

theorem :: LIMFUNC1:19
canceled;

theorem :: LIMFUNC1:20
canceled;

theorem :: LIMFUNC1:21
canceled;

theorem :: LIMFUNC1:22
canceled;

theorem :: LIMFUNC1:23
canceled;

theorem :: LIMFUNC1:24
canceled;

theorem :: LIMFUNC1:25
canceled;

theorem :: LIMFUNC1:26
for seq being Real_Sequence holds
( ( seq is non-decreasing implies seq is bounded_below ) & ( seq is non-increasing implies seq is bounded_above ) )
proof end;

theorem Th27: :: LIMFUNC1:27
for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is non-decreasing holds
for n being Element of NAT holds seq . n < 0
proof end;

theorem Th28: :: LIMFUNC1:28
for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is non-increasing holds
for n being Element of NAT holds 0 < seq . n
proof end;

theorem Th29: :: LIMFUNC1:29
for seq being Real_Sequence st seq is convergent & 0 < lim seq holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
0 < seq . m
proof end;

theorem Th30: :: LIMFUNC1:30
for seq being Real_Sequence st seq is convergent & 0 < lim seq holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(lim seq) / 2 < seq . m
proof end;

definition
let seq be Real_Sequence;
attr seq is divergent_to+infty means :Def4: :: LIMFUNC1:def 4
 for r being Real ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < seq . m;
attr seq is divergent_to-infty means :Def5: :: LIMFUNC1:def 5
 for r being Real ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq . m < r;
end;

:: deftheorem Def4 defines divergent_to+infty LIMFUNC1:def 4 :
for seq being Real_Sequence holds
( seq is divergent_to+infty iff for r being Real ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < seq . m );

:: deftheorem Def5 defines divergent_to-infty LIMFUNC1:def 5 :
for seq being Real_Sequence holds
( seq is divergent_to-infty iff for r being Real ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq . m < r );

theorem :: LIMFUNC1:31
canceled;

theorem :: LIMFUNC1:32
canceled;

theorem :: LIMFUNC1:33
for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq ^\ m is non-zero
proof end;

theorem Th34: :: LIMFUNC1:34
for k being Element of NAT
for seq being Real_Sequence holds
( ( seq ^\ k is divergent_to+infty implies seq is divergent_to+infty ) & ( seq ^\ k is divergent_to-infty implies seq is divergent_to-infty ) )
proof end;

theorem Th35: :: LIMFUNC1:35
for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is divergent_to+infty holds
seq1 + seq2 is divergent_to+infty
proof end;

theorem Th36: :: LIMFUNC1:36
for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is bounded_below holds
seq1 + seq2 is divergent_to+infty
proof end;

theorem Th37: :: LIMFUNC1:37
for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is divergent_to+infty holds
seq1 (#) seq2 is divergent_to+infty
proof end;

theorem Th38: :: LIMFUNC1:38
for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is divergent_to-infty holds
seq1 + seq2 is divergent_to-infty
proof end;

theorem Th39: :: LIMFUNC1:39
for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is bounded_above holds
seq1 + seq2 is divergent_to-infty
proof end;

theorem Th40: :: LIMFUNC1:40
for seq being Real_Sequence
for r being Real holds
( ( seq is divergent_to+infty & r > 0 implies r (#) seq is divergent_to+infty ) & ( seq is divergent_to+infty & r < 0 implies r (#) seq is divergent_to-infty ) & ( r = 0 implies ( rng (r (#) seq) = {0} & r (#) seq is constant ) ) )
proof end;

theorem Th41: :: LIMFUNC1:41
for seq being Real_Sequence
for r being Real holds
( ( seq is divergent_to-infty & r > 0 implies r (#) seq is divergent_to-infty ) & ( seq is divergent_to-infty & r < 0 implies r (#) seq is divergent_to+infty ) & ( r = 0 implies ( rng (r (#) seq) = {0} & r (#) seq is constant ) ) )
proof end;

theorem :: LIMFUNC1:42
for seq being Real_Sequence holds
( ( seq is divergent_to+infty implies - seq is divergent_to-infty ) & ( seq is divergent_to-infty implies - seq is divergent_to+infty ) )
proof end;

theorem :: LIMFUNC1:43
for seq, seq1 being Real_Sequence st seq is bounded_below & seq1 is divergent_to-infty holds
seq - seq1 is divergent_to+infty
proof end;

theorem :: LIMFUNC1:44
for seq, seq1 being Real_Sequence st seq is bounded_above & seq1 is divergent_to+infty holds
seq - seq1 is divergent_to-infty
proof end;

theorem :: LIMFUNC1:45
for seq, seq1 being Real_Sequence st seq is divergent_to+infty & seq1 is convergent holds
seq + seq1 is divergent_to+infty
proof end;

theorem :: LIMFUNC1:46
for seq, seq1 being Real_Sequence st seq is divergent_to-infty & seq1 is convergent holds
seq + seq1 is divergent_to-infty
proof end;

theorem Th47: :: LIMFUNC1:47
for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = n ) holds
seq is divergent_to+infty
proof end;

set s1 = incl NAT;

Lm4: for n being Element of NAT holds (incl NAT) . n = n
by FUNCT_1:35;

theorem Th48: :: LIMFUNC1:48
for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = - n ) holds
seq is divergent_to-infty
proof end;

theorem Th49: :: LIMFUNC1:49
for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & ex r being Real st
( r > 0 & ( for n being Element of NAT holds seq2 . n >= r ) ) holds
seq1 (#) seq2 is divergent_to+infty
proof end;

theorem :: LIMFUNC1:50
for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & ex r being Real st
( 0 < r & ( for n being Element of NAT holds seq2 . n >= r ) ) holds
seq1 (#) seq2 is divergent_to-infty
proof end;

theorem Th51: :: LIMFUNC1:51
for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is divergent_to-infty holds
seq1 (#) seq2 is divergent_to+infty
proof end;

theorem Th52: :: LIMFUNC1:52
for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds
abs seq is divergent_to+infty
proof end;

theorem Th53: :: LIMFUNC1:53
for seq, seq1 being Real_Sequence st seq is divergent_to+infty & seq1 is subsequence of seq holds
seq1 is divergent_to+infty
proof end;

theorem Th54: :: LIMFUNC1:54
for seq, seq1 being Real_Sequence st seq is divergent_to-infty & seq1 is subsequence of seq holds
seq1 is divergent_to-infty
proof end;

theorem :: LIMFUNC1:55
for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is convergent & 0 < lim seq2 holds
seq1 (#) seq2 is divergent_to+infty
proof end;

theorem Th56: :: LIMFUNC1:56
for seq being Real_Sequence st seq is non-decreasing & not seq is bounded_above holds
seq is divergent_to+infty
proof end;

theorem Th57: :: LIMFUNC1:57
for seq being Real_Sequence st seq is non-increasing & not seq is bounded_below holds
seq is divergent_to-infty
proof end;

theorem :: LIMFUNC1:58
for seq being Real_Sequence st seq is increasing & not seq is bounded_above holds
seq is divergent_to+infty by Th56;

theorem :: LIMFUNC1:59
for seq being Real_Sequence st seq is decreasing & not seq is bounded_below holds
seq is divergent_to-infty by Th57;

theorem :: LIMFUNC1:60
for seq being Real_Sequence holds
( not seq is monotone or seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )
proof end;

theorem Th61: :: LIMFUNC1:61
for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds
( seq " is convergent & lim (seq ") = 0 )
proof end;

theorem Th62: :: LIMFUNC1:62
for seq being Real_Sequence st seq is convergent & lim seq = 0 & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
0 < seq . n holds
seq " is divergent_to+infty
proof end;

theorem Th63: :: LIMFUNC1:63
for seq being Real_Sequence st seq is convergent & lim seq = 0 & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq . n < 0 holds
seq " is divergent_to-infty
proof end;

theorem Th64: :: LIMFUNC1:64
for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is non-decreasing holds
seq " is divergent_to-infty
proof end;

theorem Th65: :: LIMFUNC1:65
for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is non-increasing holds
seq " is divergent_to+infty
proof end;

theorem :: LIMFUNC1:66
for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is increasing holds
seq " is divergent_to-infty by Th64;

theorem :: LIMFUNC1:67
for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is decreasing holds
seq " is divergent_to+infty by Th65;

theorem :: LIMFUNC1:68
for seq1, seq2 being Real_Sequence st seq1 is bounded & ( seq2 is divergent_to+infty or seq2 is divergent_to-infty ) holds
( seq1 /" seq2 is convergent & lim (seq1 /" seq2) = 0 )
proof end;

theorem Th69: :: LIMFUNC1:69
for seq, seq1 being Real_Sequence st seq is divergent_to+infty & ( for n being Element of NAT holds seq . n <= seq1 . n ) holds
seq1 is divergent_to+infty
proof end;

theorem Th70: :: LIMFUNC1:70
for seq, seq1 being Real_Sequence st seq is divergent_to-infty & ( for n being Element of NAT holds seq1 . n <= seq . n ) holds
seq1 is divergent_to-infty
proof end;

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

:: deftheorem Def6 defines convergent_in+infty LIMFUNC1:def 6 :
for f being PartFunc of REAL,REAL holds
( f is convergent_in+infty iff ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex g being Real st
for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = g ) ) );

:: deftheorem Def7 defines divergent_in+infty_to+infty LIMFUNC1:def 7 :
for f being PartFunc of REAL,REAL holds
( f is divergent_in+infty_to+infty iff ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
f /* seq is divergent_to+infty ) ) );

:: deftheorem Def8 defines divergent_in+infty_to-infty LIMFUNC1:def 8 :
for f being PartFunc of REAL,REAL holds
( f is divergent_in+infty_to-infty iff ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
f /* seq is divergent_to-infty ) ) );

:: deftheorem Def9 defines convergent_in-infty LIMFUNC1:def 9 :
for f being PartFunc of REAL,REAL holds
( f is convergent_in-infty iff ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex g being Real st
for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = g ) ) );

:: deftheorem Def10 defines divergent_in-infty_to+infty LIMFUNC1:def 10 :
for f being PartFunc of REAL,REAL holds
( f is divergent_in-infty_to+infty iff ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
f /* seq is divergent_to+infty ) ) );

:: deftheorem Def11 defines divergent_in-infty_to-infty LIMFUNC1:def 11 :
for f being PartFunc of REAL,REAL holds
( f is divergent_in-infty_to-infty iff ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
f /* seq is divergent_to-infty ) ) );

theorem :: LIMFUNC1:71
canceled;

theorem :: LIMFUNC1:72
canceled;

theorem :: LIMFUNC1:73
canceled;

theorem :: LIMFUNC1:74
canceled;

theorem :: LIMFUNC1:75
canceled;

theorem :: LIMFUNC1:76
canceled;

theorem :: LIMFUNC1:77
for f being PartFunc of REAL,REAL holds
( f is convergent_in+infty iff ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
abs ((f . r1) - g) < g1 ) )
proof end;

theorem :: LIMFUNC1:78
for f being PartFunc of REAL,REAL holds
( f is convergent_in-infty iff ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
abs ((f . r1) - g) < g1 ) )
proof end;

theorem :: LIMFUNC1:79
for f being PartFunc of REAL,REAL holds
( f is divergent_in+infty_to+infty iff ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
g < f . r1 ) ) )
proof end;

theorem :: LIMFUNC1:80
for f being PartFunc of REAL,REAL holds
( f is divergent_in+infty_to-infty iff ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
f . r1 < g ) ) )
proof end;

theorem :: LIMFUNC1:81
for f being PartFunc of REAL,REAL holds
( f is divergent_in-infty_to+infty iff ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
g < f . r1 ) ) )
proof end;

theorem :: LIMFUNC1:82
for f being PartFunc of REAL,REAL holds
( f is divergent_in-infty_to-infty iff ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
f . r1 < g ) ) )
proof end;

theorem :: LIMFUNC1:83
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 f1) /\ (dom f2) ) ) holds
( f1 + f2 is divergent_in+infty_to+infty & f1 (#) f2 is divergent_in+infty_to+infty )
proof end;

theorem :: LIMFUNC1:84
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 f1) /\ (dom f2) ) ) holds
( f1 + f2 is divergent_in+infty_to-infty & f1 (#) f2 is divergent_in+infty_to+infty )
proof end;

theorem :: LIMFUNC1:85
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 f1) /\ (dom f2) ) ) holds
( f1 + f2 is divergent_in-infty_to+infty & f1 (#) f2 is divergent_in-infty_to+infty )
proof end;

theorem :: LIMFUNC1:86
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 f1) /\ (dom f2) ) ) holds
( f1 + f2 is divergent_in-infty_to-infty & f1 (#) f2 is divergent_in-infty_to+infty )
proof end;

theorem :: LIMFUNC1:87
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 + f2) ) ) & ex r being Real st f2 | (right_open_halfline r) is bounded_below holds
f1 + f2 is divergent_in+infty_to+infty
proof end;

theorem :: LIMFUNC1:88
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st
( 0 < r & ( for g being Real st g in (dom f2) /\ (right_open_halfline r1) holds
r <= f2 . g ) ) holds
f1 (#) f2 is divergent_in+infty_to+infty
proof end;

theorem :: LIMFUNC1:89
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 + f2) ) ) & ex r being Real st f2 | (left_open_halfline r) is bounded_below holds
f1 + f2 is divergent_in-infty_to+infty
proof end;

theorem :: LIMFUNC1:90
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st
( 0 < r & ( for g being Real st g in (dom f2) /\ (left_open_halfline r1) holds
r <= f2 . g ) ) holds
f1 (#) f2 is divergent_in-infty_to+infty
proof end;

theorem :: LIMFUNC1:91
for f being PartFunc of REAL,REAL
for r being Real holds
( ( f is divergent_in+infty_to+infty & r > 0 implies r (#) f is divergent_in+infty_to+infty ) & ( f is divergent_in+infty_to+infty & r < 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r > 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r < 0 implies r (#) f is divergent_in+infty_to+infty ) )
proof end;

theorem :: LIMFUNC1:92
for f being PartFunc of REAL,REAL
for r being Real holds
( ( f is divergent_in-infty_to+infty & r > 0 implies r (#) f is divergent_in-infty_to+infty ) & ( f is divergent_in-infty_to+infty & r < 0 implies r (#) f is divergent_in-infty_to-infty ) & ( f is divergent_in-infty_to-infty & r > 0 implies r (#) f is divergent_in-infty_to-infty ) & ( f is divergent_in-infty_to-infty & r < 0 implies r (#) f is divergent_in-infty_to+infty ) )
proof end;

theorem :: LIMFUNC1:93
for f being PartFunc of REAL,REAL st ( f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty ) holds
abs f is divergent_in+infty_to+infty
proof end;

theorem :: LIMFUNC1:94
for f being PartFunc of REAL,REAL st ( f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty ) holds
abs f is divergent_in-infty_to+infty
proof end;

theorem Th95: :: LIMFUNC1:95
for f being PartFunc of REAL,REAL st ex r being Real st
( f | (right_open_halfline r) is non-decreasing & not f | (right_open_halfline r) is bounded_above ) & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) holds
f is divergent_in+infty_to+infty
proof end;

theorem :: LIMFUNC1:96
for f being PartFunc of REAL,REAL st ex r being Real st
( f | (right_open_halfline r) is increasing & not f | (right_open_halfline r) is bounded_above ) & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) holds
f is divergent_in+infty_to+infty by Th95;

theorem Th97: :: LIMFUNC1:97
for f being PartFunc of REAL,REAL st ex r being Real st
( f | (right_open_halfline r) is non-increasing & not f | (right_open_halfline r) is bounded_below ) & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) holds
f is divergent_in+infty_to-infty
proof end;

theorem :: LIMFUNC1:98
for f being PartFunc of REAL,REAL st ex r being Real st
( f | (right_open_halfline r) is decreasing & not f | (right_open_halfline r) is bounded_below ) & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) holds
f is divergent_in+infty_to-infty by Th97;

theorem Th99: :: LIMFUNC1:99
for f being PartFunc of REAL,REAL st ex r being Real st
( f | (left_open_halfline r) is non-increasing & not f | (left_open_halfline r) is bounded_above ) & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) holds
f is divergent_in-infty_to+infty
proof end;

theorem :: LIMFUNC1:100
for f being PartFunc of REAL,REAL st ex r being Real st
( f | (left_open_halfline r) is decreasing & not f | (left_open_halfline r) is bounded_above ) & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) holds
f is divergent_in-infty_to+infty by Th99;

theorem Th101: :: LIMFUNC1:101
for f being PartFunc of REAL,REAL st ex r being Real st
( f | (left_open_halfline r) is non-decreasing & not f | (left_open_halfline r) is bounded_below ) & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) holds
f is divergent_in-infty_to-infty
proof end;

theorem :: LIMFUNC1:102
for f being PartFunc of REAL,REAL st ex r being Real st
( f | (left_open_halfline r) is increasing & not f | (left_open_halfline r) is bounded_below ) & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) holds
f is divergent_in-infty_to-infty by Th101;

theorem Th103: :: LIMFUNC1:103
for f1, f being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex r being Real st
( (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f) /\ (right_open_halfline r) holds
f1 . g <= f . g ) ) holds
f is divergent_in+infty_to+infty
proof end;

theorem Th104: :: LIMFUNC1:104
for f1, f being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex r being Real st
( (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f) /\ (right_open_halfline r) holds
f . g <= f1 . g ) ) holds
f is divergent_in+infty_to-infty
proof end;

theorem Th105: :: LIMFUNC1:105
for f1, f being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex r being Real st
( (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f1 . g <= f . g ) ) holds
f is divergent_in-infty_to+infty
proof end;

theorem Th106: :: LIMFUNC1:106
for f1, f being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex r being Real st
( (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f . g <= f1 . g ) ) holds
f is divergent_in-infty_to-infty
proof end;

theorem :: LIMFUNC1:107
for f1, f being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & ex r being Real st
( right_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in right_open_halfline r holds
f1 . g <= f . g ) ) holds
f is divergent_in+infty_to+infty
proof end;

theorem :: LIMFUNC1:108
for f1, f being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & ex r being Real st
( right_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in right_open_halfline r holds
f . g <= f1 . g ) ) holds
f is divergent_in+infty_to-infty
proof end;

theorem :: LIMFUNC1:109
for f1, f being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & ex r being Real st
( left_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in left_open_halfline r holds
f1 . g <= f . g ) ) holds
f is divergent_in-infty_to+infty
proof end;

theorem :: LIMFUNC1:110
for f1, f being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & ex r being Real st
( left_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in left_open_halfline r holds
f . g <= f1 . g ) ) holds
f is divergent_in-infty_to-infty
proof end;

definition
let f be PartFunc of REAL,REAL;
assume A1: f is convergent_in+infty ;
func lim_in+infty f -> Real means :Def12: :: LIMFUNC1:def 12
 for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = it );
existence
ex b1 being Real st
for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = b1 ) by A1, Def6;
uniqueness
for b1, b2 being Real st ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = b1 ) ) & ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = b2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines lim_in+infty LIMFUNC1:def 12 :
for f being PartFunc of REAL,REAL st f is convergent_in+infty holds
for b2 being Real holds
( b2 = lim_in+infty f iff for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = b2 ) );

definition
let f be PartFunc of REAL,REAL;
assume A1: f is convergent_in-infty ;
func lim_in-infty f -> Real means :Def13: :: LIMFUNC1:def 13
 for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = it );
existence
ex b1 being Real st
for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = b1 ) by A1, Def9;
uniqueness
for b1, b2 being Real st ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = b1 ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = b2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines lim_in-infty LIMFUNC1:def 13 :
for f being PartFunc of REAL,REAL st f is convergent_in-infty holds
for b2 being Real holds
( b2 = lim_in-infty f iff for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = b2 ) );

theorem :: LIMFUNC1:111
canceled;

theorem :: LIMFUNC1:112
canceled;

theorem :: LIMFUNC1:113
for f being PartFunc of REAL,REAL
for g being Real st f is convergent_in-infty holds
( lim_in-infty f = g iff for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
abs ((f . r1) - g) < g1 )
proof end;

theorem :: LIMFUNC1:114
for f being PartFunc of REAL,REAL
for g being Real st f is convergent_in+infty holds
( lim_in+infty f = g iff for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
abs ((f . r1) - g) < g1 )
proof end;

theorem Th115: :: LIMFUNC1:115
for f being PartFunc of REAL,REAL
for r being Real st f is convergent_in+infty holds
( r (#) f is convergent_in+infty & lim_in+infty (r (#) f) = r * (lim_in+infty f) )
proof end;

theorem Th116: :: LIMFUNC1:116
for f being PartFunc of REAL,REAL st f is convergent_in+infty holds
( - f is convergent_in+infty & lim_in+infty (- f) = - (lim_in+infty f) )
proof end;

theorem Th117: :: LIMFUNC1:117
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 + f2) ) ) holds
( f1 + f2 is convergent_in+infty & lim_in+infty (f1 + f2) = (lim_in+infty f1) + (lim_in+infty f2) )
proof end;

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

theorem :: LIMFUNC1:119
for f being PartFunc of REAL,REAL st f is convergent_in+infty & f " {0} = {} & lim_in+infty f <> 0 holds
( f ^ is convergent_in+infty & lim_in+infty (f ^) = (lim_in+infty f) " )
proof end;

theorem :: LIMFUNC1:120
for f being PartFunc of REAL,REAL st f is convergent_in+infty holds
( abs f is convergent_in+infty & lim_in+infty (abs f) = abs (lim_in+infty f) )
proof end;

theorem Th121: :: LIMFUNC1:121
for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f <> 0 & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ) holds
( f ^ is convergent_in+infty & lim_in+infty (f ^) = (lim_in+infty f) " )
proof end;

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

theorem :: LIMFUNC1:123
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f2 <> 0 & ( for r being Real ex g being Real st
( r < g & g in dom (f1 / f2) ) ) holds
( f1 / f2 is convergent_in+infty & lim_in+infty (f1 / f2) = (lim_in+infty f1) / (lim_in+infty f2) )
proof end;

theorem Th124: :: LIMFUNC1:124
for f being PartFunc of REAL,REAL
for r being Real st f is convergent_in-infty holds
( r (#) f is convergent_in-infty & lim_in-infty (r (#) f) = r * (lim_in-infty f) )
proof end;

theorem Th125: :: LIMFUNC1:125
for f being PartFunc of REAL,REAL st f is convergent_in-infty holds
( - f is convergent_in-infty & lim_in-infty (- f) = - (lim_in-infty f) )
proof end;

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

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

theorem :: LIMFUNC1:128
for f being PartFunc of REAL,REAL st f is convergent_in-infty & f " {0} = {} & lim_in-infty f <> 0 holds
( f ^ is convergent_in-infty & lim_in-infty (f ^) = (lim_in-infty f) " )
proof end;

theorem :: LIMFUNC1:129
for f being PartFunc of REAL,REAL st f is convergent_in-infty holds
( abs f is convergent_in-infty & lim_in-infty (abs f) = abs (lim_in-infty f) )
proof end;

theorem Th130: :: LIMFUNC1:130
for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f <> 0 & ( for r being Real ex g being Real st
( g < r & g in dom f & f . g <> 0 ) ) holds
( f ^ is convergent_in-infty & lim_in-infty (f ^) = (lim_in-infty f) " )
proof end;

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

theorem :: LIMFUNC1:132
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f2 <> 0 & ( for r being Real ex g being Real st
( g < r & g in dom (f1 / f2) ) ) holds
( f1 / f2 is convergent_in-infty & lim_in-infty (f1 / f2) = (lim_in-infty f1) / (lim_in-infty f2) )
proof end;

theorem :: LIMFUNC1:133
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & lim_in+infty f1 = 0 & ( for r being Real ex g being Real st
( r < g & g in dom (f1 (#) f2) ) ) & ex r being Real st f2 | (right_open_halfline r) is bounded holds
( f1 (#) f2 is convergent_in+infty & lim_in+infty (f1 (#) f2) = 0 )
proof end;

theorem :: LIMFUNC1:134
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & lim_in-infty f1 = 0 & ( for r being Real ex g being Real st
( g < r & g in dom (f1 (#) f2) ) ) & ex r being Real st f2 | (left_open_halfline r) is bounded holds
( f1 (#) f2 is convergent_in-infty & lim_in-infty (f1 (#) f2) = 0 )
proof end;

theorem Th135: :: LIMFUNC1:135
for f1, f2, f being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f1 = lim_in+infty f2 & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex r being Real st
( ( ( (dom f1) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) & (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) ) or ( (dom f2) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & (dom f) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) ) ) & ( for g being Real st g in (dom f) /\ (right_open_halfline r) holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 )
proof end;

theorem :: LIMFUNC1:136
for f1, f2, f being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f1 = lim_in+infty f2 & ex r being Real st
( right_open_halfline r c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in right_open_halfline r holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 )
proof end;

theorem Th137: :: LIMFUNC1:137
for f1, f2, f being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f1 = lim_in-infty f2 & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex r being Real st
( ( ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) ) or ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & (dom f) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) ) ) & ( for g being Real st g in (dom f) /\ (left_open_halfline r) holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 )
proof end;

theorem :: LIMFUNC1:138
for f1, f2, f being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f1 = lim_in-infty f2 & ex r being Real st
( left_open_halfline r c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in left_open_halfline r holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 )
proof end;

theorem :: LIMFUNC1:139
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & ex r being Real st
( ( (dom f1) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) & ( for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f2) /\ (right_open_halfline r) holds
f1 . g <= f2 . g ) ) ) holds
lim_in+infty f1 <= lim_in+infty f2
proof end;

theorem :: LIMFUNC1:140
for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & ex r being Real st
( ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & ( for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f2) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) ) holds
lim_in-infty f1 <= lim_in-infty f2
proof end;

theorem :: LIMFUNC1:141
for f being PartFunc of REAL,REAL st ( f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty ) & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ) holds
( f ^ is convergent_in+infty & lim_in+infty (f ^) = 0 )
proof end;

theorem :: LIMFUNC1:142
for f being PartFunc of REAL,REAL st ( f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty ) & ( for r being Real ex g being Real st
( g < r & g in dom f & f . g <> 0 ) ) holds
( f ^ is convergent_in-infty & lim_in-infty (f ^) = 0 )
proof end;

theorem :: LIMFUNC1:143
for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f = 0 & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ) & ex r being Real st
for g being Real st g in (dom f) /\ (right_open_halfline r) holds
0 <= f . g holds
f ^ is divergent_in+infty_to+infty
proof end;

theorem :: LIMFUNC1:144
for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f = 0 & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ) & ex r being Real st
for g being Real st g in (dom f) /\ (right_open_halfline r) holds
f . g <= 0 holds
f ^ is divergent_in+infty_to-infty
proof end;

theorem :: LIMFUNC1:145
for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f = 0 & ( for r being Real ex g being Real st
( g < r & g in dom f & f . g <> 0 ) ) & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
0 <= f . g holds
f ^ is divergent_in-infty_to+infty
proof end;

theorem :: LIMFUNC1:146
for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f = 0 & ( for r being Real ex g being Real st
( g < r & g in dom f & f . g <> 0 ) ) & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f . g <= 0 holds
f ^ is divergent_in-infty_to-infty
proof end;

theorem :: LIMFUNC1:147
for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (right_open_halfline r) holds
0 < f . g holds
f ^ is divergent_in+infty_to+infty
proof end;

theorem :: LIMFUNC1:148
for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (right_open_halfline r) holds
f . g < 0 holds
f ^ is divergent_in+infty_to-infty
proof end;

theorem :: LIMFUNC1:149
for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
0 < f . g holds
f ^ is divergent_in-infty_to+infty
proof end;

theorem :: LIMFUNC1:150
for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f . g < 0 holds
f ^ is divergent_in-infty_to-infty
proof end;