:: by Jaros{\l}aw Kotowicz

::

:: Received August 20, 1990

:: Copyright (c) 1990-2012 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 r be real number ;

coherence

].-infty,r.] is Subset of REAL

[.r,+infty.[ is Subset of REAL

].r,+infty.[ is Subset of REAL

end;
coherence

].-infty,r.] is Subset of REAL

proof end;

coherence [.r,+infty.[ is Subset of REAL

proof end;

coherence ].r,+infty.[ is Subset of REAL

proof end;

:: deftheorem defines left_closed_halfline LIMFUNC1:def 1 :

for r being real number holds left_closed_halfline r = ].-infty,r.];

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.[;

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.[;

for r being real number holds right_open_halfline r = ].r,+infty.[;

theorem :: LIMFUNC1:1

for seq being Real_Sequence holds

( ( seq is non-decreasing implies seq is bounded_below ) & ( seq is non-increasing implies seq is bounded_above ) )

( ( seq is non-decreasing implies seq is bounded_below ) & ( seq is non-increasing implies seq is bounded_above ) )

proof end;

theorem Th2: :: LIMFUNC1:2

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

for n being Element of NAT holds seq . n < 0

proof end;

theorem Th3: :: LIMFUNC1:3

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

for n being Element of NAT holds 0 < seq . n

proof end;

theorem Th4: :: LIMFUNC1:4

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

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

0 < seq . m

proof end;

theorem Th5: :: LIMFUNC1:5

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

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;

end;
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;

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 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 );

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 );

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:6

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

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 Th7: :: LIMFUNC1:7

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 ) )

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 Th8: :: LIMFUNC1:8

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is divergent_to+infty holds

seq1 + seq2 is divergent_to+infty

seq1 + seq2 is divergent_to+infty

proof end;

theorem Th9: :: LIMFUNC1:9

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is bounded_below holds

seq1 + seq2 is divergent_to+infty

seq1 + seq2 is divergent_to+infty

proof end;

theorem Th10: :: LIMFUNC1:10

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is divergent_to+infty holds

seq1 (#) seq2 is divergent_to+infty

seq1 (#) seq2 is divergent_to+infty

proof end;

theorem Th11: :: LIMFUNC1:11

for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is divergent_to-infty holds

seq1 + seq2 is divergent_to-infty

seq1 + seq2 is divergent_to-infty

proof end;

theorem Th12: :: LIMFUNC1:12

for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is bounded_above holds

seq1 + seq2 is divergent_to-infty

seq1 + seq2 is divergent_to-infty

proof end;

theorem Th13: :: LIMFUNC1:13

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 ) ) )

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 Th14: :: LIMFUNC1:14

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 ) ) )

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:15

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 ) )

( ( 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:16

for seq, seq1 being Real_Sequence st seq is bounded_below & seq1 is divergent_to-infty holds

seq - seq1 is divergent_to+infty

seq - seq1 is divergent_to+infty

proof end;

theorem :: LIMFUNC1:17

for seq, seq1 being Real_Sequence st seq is bounded_above & seq1 is divergent_to+infty holds

seq - seq1 is divergent_to-infty

seq - seq1 is divergent_to-infty

proof end;

theorem :: LIMFUNC1:18

for seq, seq1 being Real_Sequence st seq is divergent_to+infty & seq1 is convergent holds

seq + seq1 is divergent_to+infty by Th9;

seq + seq1 is divergent_to+infty by Th9;

theorem :: LIMFUNC1:19

for seq, seq1 being Real_Sequence st seq is divergent_to-infty & seq1 is convergent holds

seq + seq1 is divergent_to-infty by Th12;

seq + seq1 is divergent_to-infty by Th12;

theorem Th20: :: LIMFUNC1:20

for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = n ) holds

seq is divergent_to+infty

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:18;

theorem Th21: :: LIMFUNC1:21

for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = - n ) holds

seq is divergent_to-infty

seq is divergent_to-infty

proof end;

theorem Th22: :: LIMFUNC1:22

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

( r > 0 & ( for n being Element of NAT holds seq2 . n >= r ) ) holds

seq1 (#) seq2 is divergent_to+infty

proof end;

theorem :: LIMFUNC1:23

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

( 0 < r & ( for n being Element of NAT holds seq2 . n >= r ) ) holds

seq1 (#) seq2 is divergent_to-infty

proof end;

theorem Th24: :: LIMFUNC1:24

for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is divergent_to-infty holds

seq1 (#) seq2 is divergent_to+infty

seq1 (#) seq2 is divergent_to+infty

proof end;

theorem Th25: :: LIMFUNC1:25

for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds

abs seq is divergent_to+infty

abs seq is divergent_to+infty

proof end;

theorem Th26: :: LIMFUNC1:26

for seq, seq1 being Real_Sequence st seq is divergent_to+infty & seq1 is subsequence of seq holds

seq1 is divergent_to+infty

seq1 is divergent_to+infty

proof end;

theorem Th27: :: LIMFUNC1:27

for seq, seq1 being Real_Sequence st seq is divergent_to-infty & seq1 is subsequence of seq holds

seq1 is divergent_to-infty

seq1 is divergent_to-infty

proof end;

theorem :: LIMFUNC1:28

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

seq1 (#) seq2 is divergent_to+infty

proof end;

theorem Th29: :: LIMFUNC1:29

for seq being Real_Sequence st seq is non-decreasing & not seq is bounded_above holds

seq is divergent_to+infty

seq is divergent_to+infty

proof end;

theorem Th30: :: LIMFUNC1:30

for seq being Real_Sequence st seq is non-increasing & not seq is bounded_below holds

seq is divergent_to-infty

seq is divergent_to-infty

proof end;

theorem :: LIMFUNC1:31

for seq being Real_Sequence st seq is increasing & not seq is bounded_above holds

seq is divergent_to+infty by Th29;

seq is divergent_to+infty by Th29;

theorem :: LIMFUNC1:32

for seq being Real_Sequence st seq is decreasing & not seq is bounded_below holds

seq is divergent_to-infty by Th30;

seq is divergent_to-infty by Th30;

theorem :: LIMFUNC1:33

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 )

( not seq is monotone or seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )

proof end;

theorem Th34: :: LIMFUNC1:34

for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds

( seq " is convergent & lim (seq ") = 0 )

( seq " is convergent & lim (seq ") = 0 )

proof end;

theorem Th35: :: LIMFUNC1:35

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

for n being Element of NAT st k <= n holds

0 < seq . n holds

seq " is divergent_to+infty

proof end;

theorem Th36: :: LIMFUNC1:36

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

for n being Element of NAT st k <= n holds

seq . n < 0 holds

seq " is divergent_to-infty

proof end;

theorem Th37: :: LIMFUNC1:37

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

seq " is divergent_to-infty

proof end;

theorem Th38: :: LIMFUNC1:38

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

seq " is divergent_to+infty

proof end;

theorem :: LIMFUNC1:39

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 Th37;

seq " is divergent_to-infty by Th37;

theorem :: LIMFUNC1:40

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 Th38;

seq " is divergent_to+infty by Th38;

theorem :: LIMFUNC1:41

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 )

( seq1 /" seq2 is convergent & lim (seq1 /" seq2) = 0 )

proof end;

theorem Th42: :: LIMFUNC1:42

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

seq1 is divergent_to+infty

proof end;

theorem Th43: :: LIMFUNC1:43

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

seq1 is divergent_to-infty

proof end;

definition

let f be PartFunc of REAL,REAL;

end;
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 ) );

( ( 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 ) );

( ( 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 ) );

( ( 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 ) );

( ( 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 ) );

( ( 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 ) );

( ( 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 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 ) ) );

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 ) ) );

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 ) ) );

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 ) ) );

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 ) ) );

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 ) ) );

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:44

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 ) )

( 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:45

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 ) )

( 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:46

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 ) ) )

( 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:47

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 ) ) )

( 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:48

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 ) ) )

( 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:49

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 ) ) )

( 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:50

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 )

( 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:51

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 )

( 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:52

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 )

( 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:53

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 )

( 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:54

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

( 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:55

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

( 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:56

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

( 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:57

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

( 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:58

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 ) )

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:59

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 ) )

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:60

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

abs f is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:61

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

abs f is divergent_in-infty_to+infty

proof end;

theorem Th62: :: LIMFUNC1:62

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

( 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:63

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 Th62;

( 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 Th62;

theorem Th64: :: LIMFUNC1:64

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

( 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:65

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 Th64;

( 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 Th64;

theorem Th66: :: LIMFUNC1:66

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

( 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:67

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 Th66;

( 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 Th66;

theorem Th68: :: LIMFUNC1:68

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

( 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:69

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 Th68;

( 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 Th68;

theorem Th70: :: LIMFUNC1:70

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

( 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 Th71: :: LIMFUNC1:71

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

( 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 Th72: :: LIMFUNC1:72

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

( 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 Th73: :: LIMFUNC1:73

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

( 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:74

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

( 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:75

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

( 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:76

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

( 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:77

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

( 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 ;

ex b_{1} 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) = b_{1} )
by A1, Def6;

uniqueness

for b_{1}, b_{2} 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) = b_{1} ) ) & ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds

( f /* seq is convergent & lim (f /* seq) = b_{2} ) ) holds

b_{1} = b_{2}

end;
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 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 );

ex b

for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds

( f /* seq is convergent & lim (f /* seq) = b

uniqueness

for b

( f /* seq is convergent & lim (f /* seq) = b

( f /* seq is convergent & lim (f /* seq) = b

b

proof 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 b_{2} being Real holds

( b_{2} = 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) = b_{2} ) );

for f being PartFunc of REAL,REAL st f is convergent_in+infty holds

for b

( b

( f /* seq is convergent & lim (f /* seq) = b

definition

let f be PartFunc of REAL,REAL;

assume A1: f is convergent_in-infty ;

ex b_{1} 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) = b_{1} )
by A1, Def9;

uniqueness

for b_{1}, b_{2} 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) = b_{1} ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds

( f /* seq is convergent & lim (f /* seq) = b_{2} ) ) holds

b_{1} = b_{2}

end;
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 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 );

ex b

for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds

( f /* seq is convergent & lim (f /* seq) = b

uniqueness

for b

( f /* seq is convergent & lim (f /* seq) = b

( f /* seq is convergent & lim (f /* seq) = b

b

proof 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 b_{2} being Real holds

( b_{2} = 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) = b_{2} ) );

for f being PartFunc of REAL,REAL st f is convergent_in-infty holds

for b

( b

( f /* seq is convergent & lim (f /* seq) = b

theorem :: LIMFUNC1:78

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 )

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:79

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 )

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 Th80: :: LIMFUNC1:80

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) )

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 Th81: :: LIMFUNC1:81

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) )

( - f is convergent_in+infty & lim_in+infty (- f) = - (lim_in+infty f) )

proof end;

theorem Th82: :: LIMFUNC1:82

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) )

( 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:83

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) )

( 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:84

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) " )

( f ^ is convergent_in+infty & lim_in+infty (f ^) = (lim_in+infty f) " )

proof end;

theorem :: LIMFUNC1:85

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) )

( abs f is convergent_in+infty & lim_in+infty (abs f) = abs (lim_in+infty f) )

proof end;

theorem Th86: :: LIMFUNC1:86

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) " )

( 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 Th87: :: LIMFUNC1:87

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) )

( 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:88

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) )

( 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 Th89: :: LIMFUNC1:89

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) )

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 Th90: :: LIMFUNC1:90

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) )

( - f is convergent_in-infty & lim_in-infty (- f) = - (lim_in-infty f) )

proof end;

theorem Th91: :: LIMFUNC1:91

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) )

( 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:92

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) )

( 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:93

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) " )

( f ^ is convergent_in-infty & lim_in-infty (f ^) = (lim_in-infty f) " )

proof end;

theorem :: LIMFUNC1:94

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) )

( abs f is convergent_in-infty & lim_in-infty (abs f) = abs (lim_in-infty f) )

proof end;

theorem Th95: :: LIMFUNC1:95

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) " )

( 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 Th96: :: LIMFUNC1:96

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) )

( 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:97

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) )

( 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:98

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 )

( 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:99

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 )

( 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 Th100: :: LIMFUNC1:100

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 )

( 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:101

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 )

( 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 Th102: :: LIMFUNC1:102

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 )

( 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:103

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 )

( 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:104

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

( ( (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:105

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

( ( (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:106

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 )

( r < g & g in dom f & f . g <> 0 ) ) holds

( f ^ is convergent_in+infty & lim_in+infty (f ^) = 0 )

proof end;

theorem :: LIMFUNC1:107

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 )

( g < r & g in dom f & f . g <> 0 ) ) holds

( f ^ is convergent_in-infty & lim_in-infty (f ^) = 0 )

proof end;

theorem :: LIMFUNC1:108

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

( 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:109

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

( 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:110

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

( 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:111

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

( 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:112

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

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:113

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

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:114

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

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:115

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

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;