:: by Jaros{\l}aw Kotowicz

::

:: Received August 20, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

Lm1: for r, g, 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

for X being Subset of REAL st rng seq c= (dom (f1 (#) f2)) /\ X holds

( rng seq c= dom (f1 (#) f2) & rng seq c= X & dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 & rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X )

proof end;

Lm3: for r being Real

for n being Element of NAT holds

( r - (1 / (n + 1)) < r & r < r + (1 / (n + 1)) )

proof end;

Lm4: for seq being Real_Sequence

for f1, f2 being PartFunc of REAL,REAL

for X being Subset of REAL st rng seq c= (dom (f1 + f2)) /\ X holds

( rng seq c= dom (f1 + f2) & rng seq c= X & dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X )

proof end;

theorem Th1: :: LIMFUNC2:1

for r being Real

for seq being Real_Sequence st seq is convergent & r < lim seq holds

ex n being Element of NAT st

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

r < seq . k

for seq being Real_Sequence st seq is convergent & r < lim seq holds

ex n being Element of NAT st

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

r < seq . k

proof end;

theorem Th2: :: LIMFUNC2:2

for r being Real

for seq being Real_Sequence st seq is convergent & lim seq < r holds

ex n being Element of NAT st

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

seq . k < r

for seq being Real_Sequence st seq is convergent & lim seq < r holds

ex n being Element of NAT st

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

seq . k < r

proof end;

Lm5: for x0 being Real

for seq being Real_Sequence

for f being PartFunc of REAL,REAL st ( for g1 being Real ex r being Real st

( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds

f . r1 < g1 ) ) ) & seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

f /* seq is divergent_to-infty

proof end;

theorem Th3: :: LIMFUNC2:3

for r2, r1 being Real

for f being PartFunc of REAL,REAL st 0 < r2 & ].(r1 - r2),r1.[ c= dom f holds

for r being Real st r < r1 holds

ex g being Real st

( r < g & g < r1 & g in dom f )

for f being PartFunc of REAL,REAL st 0 < r2 & ].(r1 - r2),r1.[ c= dom f holds

for r being Real st r < r1 holds

ex g being Real st

( r < g & g < r1 & g in dom f )

proof end;

theorem Th4: :: LIMFUNC2:4

for r2, r1 being Real

for f being PartFunc of REAL,REAL st 0 < r2 & ].r1,(r1 + r2).[ c= dom f holds

for r being Real st r1 < r holds

ex g being Real st

( g < r & r1 < g & g in dom f )

for f being PartFunc of REAL,REAL st 0 < r2 & ].r1,(r1 + r2).[ c= dom f holds

for r being Real st r1 < r holds

ex g being Real st

( g < r & r1 < g & g in dom f )

proof end;

theorem Th5: :: LIMFUNC2:5

for x0 being Real

for seq being Real_Sequence

for f being PartFunc of REAL,REAL st ( for n being Element of NAT holds

( x0 - (1 / (n + 1)) < seq . n & seq . n < x0 & seq . n in dom f ) ) holds

( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (left_open_halfline x0) )

for seq being Real_Sequence

for f being PartFunc of REAL,REAL st ( for n being Element of NAT holds

( x0 - (1 / (n + 1)) < seq . n & seq . n < x0 & seq . n in dom f ) ) holds

( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (left_open_halfline x0) )

proof end;

theorem Th6: :: LIMFUNC2:6

for x0 being Real

for seq being Real_Sequence

for f being PartFunc of REAL,REAL st ( for n being Element of NAT holds

( x0 < seq . n & seq . n < x0 + (1 / (n + 1)) & seq . n in dom f ) ) holds

( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (right_open_halfline x0) )

for seq being Real_Sequence

for f being PartFunc of REAL,REAL st ( for n being Element of NAT holds

( x0 < seq . n & seq . n < x0 + (1 / (n + 1)) & seq . n in dom f ) ) holds

( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (right_open_halfline x0) )

proof end;

definition

let f be PartFunc of REAL,REAL;

let x0 be Real;

end;
let x0 be Real;

pred f is_left_convergent_in x0 means :Def1: :: LIMFUNC2:def 1

( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ex g being Real st

for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = g ) );

( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ex g being Real st

for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = g ) );

pred f is_left_divergent_to+infty_in x0 means :Def2: :: LIMFUNC2:def 2

( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

f /* seq is divergent_to+infty ) );

( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

f /* seq is divergent_to+infty ) );

pred f is_left_divergent_to-infty_in x0 means :Def3: :: LIMFUNC2:def 3

( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

f /* seq is divergent_to-infty ) );

( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

f /* seq is divergent_to-infty ) );

pred f is_right_convergent_in x0 means :Def4: :: LIMFUNC2:def 4

( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ex g being Real st

for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = g ) );

( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ex g being Real st

for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = g ) );

pred f is_right_divergent_to+infty_in x0 means :Def5: :: LIMFUNC2:def 5

( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

f /* seq is divergent_to+infty ) );

( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

f /* seq is divergent_to+infty ) );

pred f is_right_divergent_to-infty_in x0 means :Def6: :: LIMFUNC2:def 6

( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

f /* seq is divergent_to-infty ) );

( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

f /* seq is divergent_to-infty ) );

:: deftheorem Def1 defines is_left_convergent_in LIMFUNC2:def 1 :

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_left_convergent_in x0 iff ( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ex g being Real st

for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = g ) ) );

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_left_convergent_in x0 iff ( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ex g being Real st

for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = g ) ) );

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

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_left_divergent_to+infty_in x0 iff ( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

f /* seq is divergent_to+infty ) ) );

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_left_divergent_to+infty_in x0 iff ( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

f /* seq is divergent_to+infty ) ) );

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

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_left_divergent_to-infty_in x0 iff ( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

f /* seq is divergent_to-infty ) ) );

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_left_divergent_to-infty_in x0 iff ( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

f /* seq is divergent_to-infty ) ) );

:: deftheorem Def4 defines is_right_convergent_in LIMFUNC2:def 4 :

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_right_convergent_in x0 iff ( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ex g being Real st

for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = g ) ) );

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_right_convergent_in x0 iff ( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ex g being Real st

for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = g ) ) );

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

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_right_divergent_to+infty_in x0 iff ( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

f /* seq is divergent_to+infty ) ) );

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_right_divergent_to+infty_in x0 iff ( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

f /* seq is divergent_to+infty ) ) );

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

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_right_divergent_to-infty_in x0 iff ( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

f /* seq is divergent_to-infty ) ) );

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_right_divergent_to-infty_in x0 iff ( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

f /* seq is divergent_to-infty ) ) );

theorem :: LIMFUNC2:7

for x0 being Real

for f being PartFunc of REAL,REAL holds

( f is_left_convergent_in x0 iff ( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ex g being Real st

for g1 being Real st 0 < g1 holds

ex r being Real st

( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds

abs ((f . r1) - g) < g1 ) ) ) )

for f being PartFunc of REAL,REAL holds

( f is_left_convergent_in x0 iff ( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ex g being Real st

for g1 being Real st 0 < g1 holds

ex r being Real st

( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds

abs ((f . r1) - g) < g1 ) ) ) )

proof end;

theorem :: LIMFUNC2:8

for x0 being Real

for f being PartFunc of REAL,REAL holds

( f is_left_divergent_to+infty_in x0 iff ( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ( for g1 being Real ex r being Real st

( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds

g1 < f . r1 ) ) ) ) )

for f being PartFunc of REAL,REAL holds

( f is_left_divergent_to+infty_in x0 iff ( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ( for g1 being Real ex r being Real st

( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds

g1 < f . r1 ) ) ) ) )

proof end;

theorem :: LIMFUNC2:9

for x0 being Real

for f being PartFunc of REAL,REAL holds

( f is_left_divergent_to-infty_in x0 iff ( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ( for g1 being Real ex r being Real st

( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds

f . r1 < g1 ) ) ) ) )

for f being PartFunc of REAL,REAL holds

( f is_left_divergent_to-infty_in x0 iff ( ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ( for g1 being Real ex r being Real st

( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds

f . r1 < g1 ) ) ) ) )

proof end;

theorem :: LIMFUNC2:10

for x0 being Real

for f being PartFunc of REAL,REAL holds

( f is_right_convergent_in x0 iff ( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ex g being Real st

for g1 being Real st 0 < g1 holds

ex r being Real st

( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds

abs ((f . r1) - g) < g1 ) ) ) )

for f being PartFunc of REAL,REAL holds

( f is_right_convergent_in x0 iff ( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ex g being Real st

for g1 being Real st 0 < g1 holds

ex r being Real st

( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds

abs ((f . r1) - g) < g1 ) ) ) )

proof end;

theorem :: LIMFUNC2:11

for x0 being Real

for f being PartFunc of REAL,REAL holds

( f is_right_divergent_to+infty_in x0 iff ( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ( for g1 being Real ex r being Real st

( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds

g1 < f . r1 ) ) ) ) )

for f being PartFunc of REAL,REAL holds

( f is_right_divergent_to+infty_in x0 iff ( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ( for g1 being Real ex r being Real st

( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds

g1 < f . r1 ) ) ) ) )

proof end;

theorem :: LIMFUNC2:12

for x0 being Real

for f being PartFunc of REAL,REAL holds

( f is_right_divergent_to-infty_in x0 iff ( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ( for g1 being Real ex r being Real st

( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds

f . r1 < g1 ) ) ) ) )

for f being PartFunc of REAL,REAL holds

( f is_right_divergent_to-infty_in x0 iff ( ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ( for g1 being Real ex r being Real st

( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds

f . r1 < g1 ) ) ) ) )

proof end;

theorem :: LIMFUNC2:13

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & f2 is_left_divergent_to+infty_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in (dom f1) /\ (dom f2) ) ) holds

( f1 + f2 is_left_divergent_to+infty_in x0 & f1 (#) f2 is_left_divergent_to+infty_in x0 )

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & f2 is_left_divergent_to+infty_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in (dom f1) /\ (dom f2) ) ) holds

( f1 + f2 is_left_divergent_to+infty_in x0 & f1 (#) f2 is_left_divergent_to+infty_in x0 )

proof end;

theorem :: LIMFUNC2:14

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to-infty_in x0 & f2 is_left_divergent_to-infty_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in (dom f1) /\ (dom f2) ) ) holds

( f1 + f2 is_left_divergent_to-infty_in x0 & f1 (#) f2 is_left_divergent_to+infty_in x0 )

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to-infty_in x0 & f2 is_left_divergent_to-infty_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in (dom f1) /\ (dom f2) ) ) holds

( f1 + f2 is_left_divergent_to-infty_in x0 & f1 (#) f2 is_left_divergent_to+infty_in x0 )

proof end;

theorem :: LIMFUNC2:15

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & f2 is_right_divergent_to+infty_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in (dom f1) /\ (dom f2) ) ) holds

( f1 + f2 is_right_divergent_to+infty_in x0 & f1 (#) f2 is_right_divergent_to+infty_in x0 )

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & f2 is_right_divergent_to+infty_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in (dom f1) /\ (dom f2) ) ) holds

( f1 + f2 is_right_divergent_to+infty_in x0 & f1 (#) f2 is_right_divergent_to+infty_in x0 )

proof end;

theorem :: LIMFUNC2:16

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to-infty_in x0 & f2 is_right_divergent_to-infty_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in (dom f1) /\ (dom f2) ) ) holds

( f1 + f2 is_right_divergent_to-infty_in x0 & f1 (#) f2 is_right_divergent_to+infty_in x0 )

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to-infty_in x0 & f2 is_right_divergent_to-infty_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in (dom f1) /\ (dom f2) ) ) holds

( f1 + f2 is_right_divergent_to-infty_in x0 & f1 (#) f2 is_right_divergent_to+infty_in x0 )

proof end;

theorem :: LIMFUNC2:17

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom (f1 + f2) ) ) & ex r being Real st

( 0 < r & f2 | ].(x0 - r),x0.[ is bounded_below ) holds

f1 + f2 is_left_divergent_to+infty_in x0

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom (f1 + f2) ) ) & ex r being Real st

( 0 < r & f2 | ].(x0 - r),x0.[ is bounded_below ) holds

f1 + f2 is_left_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC2:18

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st

( 0 < r & 0 < r1 & ( for g being Real st g in (dom f2) /\ ].(x0 - r),x0.[ holds

r1 <= f2 . g ) ) holds

f1 (#) f2 is_left_divergent_to+infty_in x0

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st

( 0 < r & 0 < r1 & ( for g being Real st g in (dom f2) /\ ].(x0 - r),x0.[ holds

r1 <= f2 . g ) ) holds

f1 (#) f2 is_left_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC2:19

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom (f1 + f2) ) ) & ex r being Real st

( 0 < r & f2 | ].x0,(x0 + r).[ is bounded_below ) holds

f1 + f2 is_right_divergent_to+infty_in x0

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom (f1 + f2) ) ) & ex r being Real st

( 0 < r & f2 | ].x0,(x0 + r).[ is bounded_below ) holds

f1 + f2 is_right_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC2:20

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st

( 0 < r & 0 < r1 & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds

r1 <= f2 . g ) ) holds

f1 (#) f2 is_right_divergent_to+infty_in x0

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st

( 0 < r & 0 < r1 & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds

r1 <= f2 . g ) ) holds

f1 (#) f2 is_right_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC2:21

for x0, r being Real

for f being PartFunc of REAL,REAL holds

( ( f is_left_divergent_to+infty_in x0 & r > 0 implies r (#) f is_left_divergent_to+infty_in x0 ) & ( f is_left_divergent_to+infty_in x0 & r < 0 implies r (#) f is_left_divergent_to-infty_in x0 ) & ( f is_left_divergent_to-infty_in x0 & r > 0 implies r (#) f is_left_divergent_to-infty_in x0 ) & ( f is_left_divergent_to-infty_in x0 & r < 0 implies r (#) f is_left_divergent_to+infty_in x0 ) )

for f being PartFunc of REAL,REAL holds

( ( f is_left_divergent_to+infty_in x0 & r > 0 implies r (#) f is_left_divergent_to+infty_in x0 ) & ( f is_left_divergent_to+infty_in x0 & r < 0 implies r (#) f is_left_divergent_to-infty_in x0 ) & ( f is_left_divergent_to-infty_in x0 & r > 0 implies r (#) f is_left_divergent_to-infty_in x0 ) & ( f is_left_divergent_to-infty_in x0 & r < 0 implies r (#) f is_left_divergent_to+infty_in x0 ) )

proof end;

theorem :: LIMFUNC2:22

for x0, r being Real

for f being PartFunc of REAL,REAL holds

( ( f is_right_divergent_to+infty_in x0 & r > 0 implies r (#) f is_right_divergent_to+infty_in x0 ) & ( f is_right_divergent_to+infty_in x0 & r < 0 implies r (#) f is_right_divergent_to-infty_in x0 ) & ( f is_right_divergent_to-infty_in x0 & r > 0 implies r (#) f is_right_divergent_to-infty_in x0 ) & ( f is_right_divergent_to-infty_in x0 & r < 0 implies r (#) f is_right_divergent_to+infty_in x0 ) )

for f being PartFunc of REAL,REAL holds

( ( f is_right_divergent_to+infty_in x0 & r > 0 implies r (#) f is_right_divergent_to+infty_in x0 ) & ( f is_right_divergent_to+infty_in x0 & r < 0 implies r (#) f is_right_divergent_to-infty_in x0 ) & ( f is_right_divergent_to-infty_in x0 & r > 0 implies r (#) f is_right_divergent_to-infty_in x0 ) & ( f is_right_divergent_to-infty_in x0 & r < 0 implies r (#) f is_right_divergent_to+infty_in x0 ) )

proof end;

theorem :: LIMFUNC2:23

for x0 being Real

for f being PartFunc of REAL,REAL st ( f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0 ) holds

abs f is_left_divergent_to+infty_in x0

for f being PartFunc of REAL,REAL st ( f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0 ) holds

abs f is_left_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC2:24

for x0 being Real

for f being PartFunc of REAL,REAL st ( f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) holds

abs f is_right_divergent_to+infty_in x0

for f being PartFunc of REAL,REAL st ( f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) holds

abs f is_right_divergent_to+infty_in x0

proof end;

theorem Th25: :: LIMFUNC2:25

for x0 being Real

for f being PartFunc of REAL,REAL st ex r being Real st

( f | ].(x0 - r),x0.[ is non-decreasing & not f | ].(x0 - r),x0.[ is bounded_above ) & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) holds

f is_left_divergent_to+infty_in x0

for f being PartFunc of REAL,REAL st ex r being Real st

( f | ].(x0 - r),x0.[ is non-decreasing & not f | ].(x0 - r),x0.[ is bounded_above ) & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) holds

f is_left_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC2:26

for x0 being Real

for f being PartFunc of REAL,REAL st ex r being Real st

( 0 < r & f | ].(x0 - r),x0.[ is increasing & not f | ].(x0 - r),x0.[ is bounded_above ) & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) holds

f is_left_divergent_to+infty_in x0 by Th25;

for f being PartFunc of REAL,REAL st ex r being Real st

( 0 < r & f | ].(x0 - r),x0.[ is increasing & not f | ].(x0 - r),x0.[ is bounded_above ) & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) holds

f is_left_divergent_to+infty_in x0 by Th25;

theorem Th27: :: LIMFUNC2:27

for x0 being Real

for f being PartFunc of REAL,REAL st ex r being Real st

( f | ].(x0 - r),x0.[ is non-increasing & not f | ].(x0 - r),x0.[ is bounded_below ) & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) holds

f is_left_divergent_to-infty_in x0

for f being PartFunc of REAL,REAL st ex r being Real st

( f | ].(x0 - r),x0.[ is non-increasing & not f | ].(x0 - r),x0.[ is bounded_below ) & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) holds

f is_left_divergent_to-infty_in x0

proof end;

theorem :: LIMFUNC2:28

for x0 being Real

for f being PartFunc of REAL,REAL st ex r being Real st

( 0 < r & f | ].(x0 - r),x0.[ is decreasing & not f | ].(x0 - r),x0.[ is bounded_below ) & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) holds

f is_left_divergent_to-infty_in x0 by Th27;

for f being PartFunc of REAL,REAL st ex r being Real st

( 0 < r & f | ].(x0 - r),x0.[ is decreasing & not f | ].(x0 - r),x0.[ is bounded_below ) & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) holds

f is_left_divergent_to-infty_in x0 by Th27;

theorem Th29: :: LIMFUNC2:29

for x0 being Real

for f being PartFunc of REAL,REAL st ex r being Real st

( f | ].x0,(x0 + r).[ is non-increasing & not f | ].x0,(x0 + r).[ is bounded_above ) & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) holds

f is_right_divergent_to+infty_in x0

for f being PartFunc of REAL,REAL st ex r being Real st

( f | ].x0,(x0 + r).[ is non-increasing & not f | ].x0,(x0 + r).[ is bounded_above ) & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) holds

f is_right_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC2:30

for x0 being Real

for f being PartFunc of REAL,REAL st ex r being Real st

( 0 < r & f | ].x0,(x0 + r).[ is decreasing & not f | ].x0,(x0 + r).[ is bounded_above ) & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) holds

f is_right_divergent_to+infty_in x0 by Th29;

for f being PartFunc of REAL,REAL st ex r being Real st

( 0 < r & f | ].x0,(x0 + r).[ is decreasing & not f | ].x0,(x0 + r).[ is bounded_above ) & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) holds

f is_right_divergent_to+infty_in x0 by Th29;

theorem Th31: :: LIMFUNC2:31

for x0 being Real

for f being PartFunc of REAL,REAL st ex r being Real st

( f | ].x0,(x0 + r).[ is non-decreasing & not f | ].x0,(x0 + r).[ is bounded_below ) & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) holds

f is_right_divergent_to-infty_in x0

for f being PartFunc of REAL,REAL st ex r being Real st

( f | ].x0,(x0 + r).[ is non-decreasing & not f | ].x0,(x0 + r).[ is bounded_below ) & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) holds

f is_right_divergent_to-infty_in x0

proof end;

theorem :: LIMFUNC2:32

for x0 being Real

for f being PartFunc of REAL,REAL st ex r being Real st

( 0 < r & f | ].x0,(x0 + r).[ is increasing & not f | ].x0,(x0 + r).[ is bounded_below ) & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) holds

f is_right_divergent_to-infty_in x0 by Th31;

for f being PartFunc of REAL,REAL st ex r being Real st

( 0 < r & f | ].x0,(x0 + r).[ is increasing & not f | ].x0,(x0 + r).[ is bounded_below ) & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) holds

f is_right_divergent_to-infty_in x0 by Th31;

theorem Th33: :: LIMFUNC2:33

for x0 being Real

for f1, f being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ex r being Real st

( 0 < r & (dom f) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds

f1 . g <= f . g ) ) holds

f is_left_divergent_to+infty_in x0

for f1, f being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ex r being Real st

( 0 < r & (dom f) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds

f1 . g <= f . g ) ) holds

f is_left_divergent_to+infty_in x0

proof end;

theorem Th34: :: LIMFUNC2:34

for x0 being Real

for f1, f being PartFunc of REAL,REAL st f1 is_left_divergent_to-infty_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ex r being Real st

( 0 < r & (dom f) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds

f . g <= f1 . g ) ) holds

f is_left_divergent_to-infty_in x0

for f1, f being PartFunc of REAL,REAL st f1 is_left_divergent_to-infty_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ex r being Real st

( 0 < r & (dom f) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds

f . g <= f1 . g ) ) holds

f is_left_divergent_to-infty_in x0

proof end;

theorem Th35: :: LIMFUNC2:35

for x0 being Real

for f1, f being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ex r being Real st

( 0 < r & (dom f) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds

f1 . g <= f . g ) ) holds

f is_right_divergent_to+infty_in x0

for f1, f being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ex r being Real st

( 0 < r & (dom f) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds

f1 . g <= f . g ) ) holds

f is_right_divergent_to+infty_in x0

proof end;

theorem Th36: :: LIMFUNC2:36

for x0 being Real

for f1, f being PartFunc of REAL,REAL st f1 is_right_divergent_to-infty_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ex r being Real st

( 0 < r & (dom f) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds

f . g <= f1 . g ) ) holds

f is_right_divergent_to-infty_in x0

for f1, f being PartFunc of REAL,REAL st f1 is_right_divergent_to-infty_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ex r being Real st

( 0 < r & (dom f) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds

f . g <= f1 . g ) ) holds

f is_right_divergent_to-infty_in x0

proof end;

theorem :: LIMFUNC2:37

for x0 being Real

for f1, f being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & ex r being Real st

( 0 < r & ].(x0 - r),x0.[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].(x0 - r),x0.[ holds

f1 . g <= f . g ) ) holds

f is_left_divergent_to+infty_in x0

for f1, f being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & ex r being Real st

( 0 < r & ].(x0 - r),x0.[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].(x0 - r),x0.[ holds

f1 . g <= f . g ) ) holds

f is_left_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC2:38

for x0 being Real

for f1, f being PartFunc of REAL,REAL st f1 is_left_divergent_to-infty_in x0 & ex r being Real st

( 0 < r & ].(x0 - r),x0.[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].(x0 - r),x0.[ holds

f . g <= f1 . g ) ) holds

f is_left_divergent_to-infty_in x0

for f1, f being PartFunc of REAL,REAL st f1 is_left_divergent_to-infty_in x0 & ex r being Real st

( 0 < r & ].(x0 - r),x0.[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].(x0 - r),x0.[ holds

f . g <= f1 . g ) ) holds

f is_left_divergent_to-infty_in x0

proof end;

theorem :: LIMFUNC2:39

for x0 being Real

for f1, f being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & ex r being Real st

( 0 < r & ].x0,(x0 + r).[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].x0,(x0 + r).[ holds

f1 . g <= f . g ) ) holds

f is_right_divergent_to+infty_in x0

for f1, f being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & ex r being Real st

( 0 < r & ].x0,(x0 + r).[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].x0,(x0 + r).[ holds

f1 . g <= f . g ) ) holds

f is_right_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC2:40

for x0 being Real

for f1, f being PartFunc of REAL,REAL st f1 is_right_divergent_to-infty_in x0 & ex r being Real st

( 0 < r & ].x0,(x0 + r).[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].x0,(x0 + r).[ holds

f . g <= f1 . g ) ) holds

f is_right_divergent_to-infty_in x0

for f1, f being PartFunc of REAL,REAL st f1 is_right_divergent_to-infty_in x0 & ex r being Real st

( 0 < r & ].x0,(x0 + r).[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].x0,(x0 + r).[ holds

f . g <= f1 . g ) ) holds

f is_right_divergent_to-infty_in x0

proof end;

definition

let f be PartFunc of REAL,REAL;

let x0 be Real;

assume A1: f is_left_convergent_in x0 ;

ex b_{1} being Real st

for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = b_{1} )
by A1, Def1;

uniqueness

for b_{1}, b_{2} being Real st ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = b_{1} ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

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

b_{1} = b_{2}

end;
let x0 be Real;

assume A1: f is_left_convergent_in x0 ;

func lim_left (f,x0) -> Real means :Def7: :: LIMFUNC2:def 7

for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = it );

existence for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = it );

ex b

for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) 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 Def7 defines lim_left LIMFUNC2:def 7 :

for f being PartFunc of REAL,REAL

for x0 being Real st f is_left_convergent_in x0 holds

for b_{3} being Real holds

( b_{3} = lim_left (f,x0) iff for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = b_{3} ) );

for f being PartFunc of REAL,REAL

for x0 being Real st f is_left_convergent_in x0 holds

for b

( b

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

definition

let f be PartFunc of REAL,REAL;

let x0 be Real;

assume A1: f is_right_convergent_in x0 ;

ex b_{1} being Real st

for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = b_{1} )
by A1, Def4;

uniqueness

for b_{1}, b_{2} being Real st ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = b_{1} ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

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

b_{1} = b_{2}

end;
let x0 be Real;

assume A1: f is_right_convergent_in x0 ;

func lim_right (f,x0) -> Real means :Def8: :: LIMFUNC2:def 8

for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = it );

existence for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = it );

ex b

for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) 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 Def8 defines lim_right LIMFUNC2:def 8 :

for f being PartFunc of REAL,REAL

for x0 being Real st f is_right_convergent_in x0 holds

for b_{3} being Real holds

( b_{3} = lim_right (f,x0) iff for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds

( f /* seq is convergent & lim (f /* seq) = b_{3} ) );

for f being PartFunc of REAL,REAL

for x0 being Real st f is_right_convergent_in x0 holds

for b

( b

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

theorem :: LIMFUNC2:41

for x0, g being Real

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 holds

( lim_left (f,x0) = g iff for g1 being Real st 0 < g1 holds

ex r being Real st

( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds

abs ((f . r1) - g) < g1 ) ) )

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 holds

( lim_left (f,x0) = g iff for g1 being Real st 0 < g1 holds

ex r being Real st

( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds

abs ((f . r1) - g) < g1 ) ) )

proof end;

theorem :: LIMFUNC2:42

for x0, g being Real

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 holds

( lim_right (f,x0) = g iff for g1 being Real st 0 < g1 holds

ex r being Real st

( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds

abs ((f . r1) - g) < g1 ) ) )

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 holds

( lim_right (f,x0) = g iff for g1 being Real st 0 < g1 holds

ex r being Real st

( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds

abs ((f . r1) - g) < g1 ) ) )

proof end;

theorem Th43: :: LIMFUNC2:43

for x0, r being Real

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 holds

( r (#) f is_left_convergent_in x0 & lim_left ((r (#) f),x0) = r * (lim_left (f,x0)) )

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 holds

( r (#) f is_left_convergent_in x0 & lim_left ((r (#) f),x0) = r * (lim_left (f,x0)) )

proof end;

theorem Th44: :: LIMFUNC2:44

for x0 being Real

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 holds

( - f is_left_convergent_in x0 & lim_left ((- f),x0) = - (lim_left (f,x0)) )

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 holds

( - f is_left_convergent_in x0 & lim_left ((- f),x0) = - (lim_left (f,x0)) )

proof end;

theorem Th45: :: LIMFUNC2:45

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom (f1 + f2) ) ) holds

( f1 + f2 is_left_convergent_in x0 & lim_left ((f1 + f2),x0) = (lim_left (f1,x0)) + (lim_left (f2,x0)) )

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom (f1 + f2) ) ) holds

( f1 + f2 is_left_convergent_in x0 & lim_left ((f1 + f2),x0) = (lim_left (f1,x0)) + (lim_left (f2,x0)) )

proof end;

theorem :: LIMFUNC2:46

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom (f1 - f2) ) ) holds

( f1 - f2 is_left_convergent_in x0 & lim_left ((f1 - f2),x0) = (lim_left (f1,x0)) - (lim_left (f2,x0)) )

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom (f1 - f2) ) ) holds

( f1 - f2 is_left_convergent_in x0 & lim_left ((f1 - f2),x0) = (lim_left (f1,x0)) - (lim_left (f2,x0)) )

proof end;

theorem :: LIMFUNC2:47

for x0 being Real

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & f " {0} = {} & lim_left (f,x0) <> 0 holds

( f ^ is_left_convergent_in x0 & lim_left ((f ^),x0) = (lim_left (f,x0)) " )

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & f " {0} = {} & lim_left (f,x0) <> 0 holds

( f ^ is_left_convergent_in x0 & lim_left ((f ^),x0) = (lim_left (f,x0)) " )

proof end;

theorem :: LIMFUNC2:48

for x0 being Real

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 holds

( abs f is_left_convergent_in x0 & lim_left ((abs f),x0) = abs (lim_left (f,x0)) )

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 holds

( abs f is_left_convergent_in x0 & lim_left ((abs f),x0) = abs (lim_left (f,x0)) )

proof end;

theorem Th49: :: LIMFUNC2:49

for x0 being Real

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & lim_left (f,x0) <> 0 & ( for r being Real st r < x0 holds

ex g being Real st

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

( f ^ is_left_convergent_in x0 & lim_left ((f ^),x0) = (lim_left (f,x0)) " )

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & lim_left (f,x0) <> 0 & ( for r being Real st r < x0 holds

ex g being Real st

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

( f ^ is_left_convergent_in x0 & lim_left ((f ^),x0) = (lim_left (f,x0)) " )

proof end;

theorem Th50: :: LIMFUNC2:50

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom (f1 (#) f2) ) ) holds

( f1 (#) f2 is_left_convergent_in x0 & lim_left ((f1 (#) f2),x0) = (lim_left (f1,x0)) * (lim_left (f2,x0)) )

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom (f1 (#) f2) ) ) holds

( f1 (#) f2 is_left_convergent_in x0 & lim_left ((f1 (#) f2),x0) = (lim_left (f1,x0)) * (lim_left (f2,x0)) )

proof end;

theorem :: LIMFUNC2:51

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left (f2,x0) <> 0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom (f1 / f2) ) ) holds

( f1 / f2 is_left_convergent_in x0 & lim_left ((f1 / f2),x0) = (lim_left (f1,x0)) / (lim_left (f2,x0)) )

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left (f2,x0) <> 0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom (f1 / f2) ) ) holds

( f1 / f2 is_left_convergent_in x0 & lim_left ((f1 / f2),x0) = (lim_left (f1,x0)) / (lim_left (f2,x0)) )

proof end;

theorem Th52: :: LIMFUNC2:52

for x0, r being Real

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 holds

( r (#) f is_right_convergent_in x0 & lim_right ((r (#) f),x0) = r * (lim_right (f,x0)) )

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 holds

( r (#) f is_right_convergent_in x0 & lim_right ((r (#) f),x0) = r * (lim_right (f,x0)) )

proof end;

theorem Th53: :: LIMFUNC2:53

for x0 being Real

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 holds

( - f is_right_convergent_in x0 & lim_right ((- f),x0) = - (lim_right (f,x0)) )

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 holds

( - f is_right_convergent_in x0 & lim_right ((- f),x0) = - (lim_right (f,x0)) )

proof end;

theorem Th54: :: LIMFUNC2:54

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom (f1 + f2) ) ) holds

( f1 + f2 is_right_convergent_in x0 & lim_right ((f1 + f2),x0) = (lim_right (f1,x0)) + (lim_right (f2,x0)) )

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom (f1 + f2) ) ) holds

( f1 + f2 is_right_convergent_in x0 & lim_right ((f1 + f2),x0) = (lim_right (f1,x0)) + (lim_right (f2,x0)) )

proof end;

theorem :: LIMFUNC2:55

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom (f1 - f2) ) ) holds

( f1 - f2 is_right_convergent_in x0 & lim_right ((f1 - f2),x0) = (lim_right (f1,x0)) - (lim_right (f2,x0)) )

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom (f1 - f2) ) ) holds

( f1 - f2 is_right_convergent_in x0 & lim_right ((f1 - f2),x0) = (lim_right (f1,x0)) - (lim_right (f2,x0)) )

proof end;

theorem :: LIMFUNC2:56

for x0 being Real

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 & f " {0} = {} & lim_right (f,x0) <> 0 holds

( f ^ is_right_convergent_in x0 & lim_right ((f ^),x0) = (lim_right (f,x0)) " )

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 & f " {0} = {} & lim_right (f,x0) <> 0 holds

( f ^ is_right_convergent_in x0 & lim_right ((f ^),x0) = (lim_right (f,x0)) " )

proof end;

theorem :: LIMFUNC2:57

for x0 being Real

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 holds

( abs f is_right_convergent_in x0 & lim_right ((abs f),x0) = abs (lim_right (f,x0)) )

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 holds

( abs f is_right_convergent_in x0 & lim_right ((abs f),x0) = abs (lim_right (f,x0)) )

proof end;

theorem Th58: :: LIMFUNC2:58

for x0 being Real

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 & lim_right (f,x0) <> 0 & ( for r being Real st x0 < r holds

ex g being Real st

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

( f ^ is_right_convergent_in x0 & lim_right ((f ^),x0) = (lim_right (f,x0)) " )

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 & lim_right (f,x0) <> 0 & ( for r being Real st x0 < r holds

ex g being Real st

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

( f ^ is_right_convergent_in x0 & lim_right ((f ^),x0) = (lim_right (f,x0)) " )

proof end;

theorem Th59: :: LIMFUNC2:59

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom (f1 (#) f2) ) ) holds

( f1 (#) f2 is_right_convergent_in x0 & lim_right ((f1 (#) f2),x0) = (lim_right (f1,x0)) * (lim_right (f2,x0)) )

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom (f1 (#) f2) ) ) holds

( f1 (#) f2 is_right_convergent_in x0 & lim_right ((f1 (#) f2),x0) = (lim_right (f1,x0)) * (lim_right (f2,x0)) )

proof end;

theorem :: LIMFUNC2:60

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & lim_right (f2,x0) <> 0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom (f1 / f2) ) ) holds

( f1 / f2 is_right_convergent_in x0 & lim_right ((f1 / f2),x0) = (lim_right (f1,x0)) / (lim_right (f2,x0)) )

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & lim_right (f2,x0) <> 0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom (f1 / f2) ) ) holds

( f1 / f2 is_right_convergent_in x0 & lim_right ((f1 / f2),x0) = (lim_right (f1,x0)) / (lim_right (f2,x0)) )

proof end;

theorem :: LIMFUNC2:61

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & lim_left (f1,x0) = 0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom (f1 (#) f2) ) ) & ex r being Real st

( 0 < r & f2 | ].(x0 - r),x0.[ is bounded ) holds

( f1 (#) f2 is_left_convergent_in x0 & lim_left ((f1 (#) f2),x0) = 0 )

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & lim_left (f1,x0) = 0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom (f1 (#) f2) ) ) & ex r being Real st

( 0 < r & f2 | ].(x0 - r),x0.[ is bounded ) holds

( f1 (#) f2 is_left_convergent_in x0 & lim_left ((f1 (#) f2),x0) = 0 )

proof end;

theorem :: LIMFUNC2:62

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & lim_right (f1,x0) = 0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom (f1 (#) f2) ) ) & ex r being Real st

( 0 < r & f2 | ].x0,(x0 + r).[ is bounded ) holds

( f1 (#) f2 is_right_convergent_in x0 & lim_right ((f1 (#) f2),x0) = 0 )

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & lim_right (f1,x0) = 0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom (f1 (#) f2) ) ) & ex r being Real st

( 0 < r & f2 | ].x0,(x0 + r).[ is bounded ) holds

( f1 (#) f2 is_right_convergent_in x0 & lim_right ((f1 (#) f2),x0) = 0 )

proof end;

theorem Th63: :: LIMFUNC2:63

for x0 being Real

for f1, f2, f being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left (f1,x0) = lim_left (f2,x0) & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds

( f1 . g <= f . g & f . g <= f2 . g ) ) & ( ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ ) or ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ ) ) ) holds

( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )

for f1, f2, f being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left (f1,x0) = lim_left (f2,x0) & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f ) ) & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds

( f1 . g <= f . g & f . g <= f2 . g ) ) & ( ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ ) or ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ ) ) ) holds

( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )

proof end;

theorem :: LIMFUNC2:64

for x0 being Real

for f1, f2, f being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left (f1,x0) = lim_left (f2,x0) & ex r being Real st

( 0 < r & ].(x0 - r),x0.[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].(x0 - r),x0.[ holds

( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds

( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )

for f1, f2, f being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left (f1,x0) = lim_left (f2,x0) & ex r being Real st

( 0 < r & ].(x0 - r),x0.[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].(x0 - r),x0.[ holds

( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds

( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )

proof end;

theorem Th65: :: LIMFUNC2:65

for x0 being Real

for f1, f2, f being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & lim_right (f1,x0) = lim_right (f2,x0) & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds

( f1 . g <= f . g & f . g <= f2 . g ) ) & ( ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & (dom f) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ ) or ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & (dom f) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ ) ) ) holds

( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )

for f1, f2, f being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & lim_right (f1,x0) = lim_right (f2,x0) & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f ) ) & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds

( f1 . g <= f . g & f . g <= f2 . g ) ) & ( ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & (dom f) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ ) or ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & (dom f) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ ) ) ) holds

( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )

proof end;

theorem :: LIMFUNC2:66

for x0 being Real

for f1, f2, f being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & lim_right (f1,x0) = lim_right (f2,x0) & ex r being Real st

( 0 < r & ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].x0,(x0 + r).[ holds

( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds

( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )

for f1, f2, f being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & lim_right (f1,x0) = lim_right (f2,x0) & ex r being Real st

( 0 < r & ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].x0,(x0 + r).[ holds

( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds

( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )

proof end;

theorem :: LIMFUNC2:67

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & ex r being Real st

( 0 < r & ( ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f1) /\ ].(x0 - r),x0.[ holds

f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f2) /\ ].(x0 - r),x0.[ holds

f1 . g <= f2 . g ) ) ) ) holds

lim_left (f1,x0) <= lim_left (f2,x0)

for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & ex r being Real st

( 0 < r & ( ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f1) /\ ].(x0 - r),x0.[ holds

f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & ( for g being Real st g in (dom f2) /\ ].(x0 - r),x0.[ holds

f1 . g <= f2 . g ) ) ) ) holds

lim_left (f1,x0) <= lim_left (f2,x0)

proof end;

theorem :: LIMFUNC2:68

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ex r being Real st

( 0 < r & ( ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f1) /\ ].x0,(x0 + r).[ holds

f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds

f1 . g <= f2 . g ) ) ) ) holds

lim_right (f1,x0) <= lim_right (f2,x0)

for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ex r being Real st

( 0 < r & ( ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f1) /\ ].x0,(x0 + r).[ holds

f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds

f1 . g <= f2 . g ) ) ) ) holds

lim_right (f1,x0) <= lim_right (f2,x0)

proof end;

theorem :: LIMFUNC2:69

for x0 being Real

for f being PartFunc of REAL,REAL st ( f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0 ) & ( for r being Real st r < x0 holds

ex g being Real st

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

( f ^ is_left_convergent_in x0 & lim_left ((f ^),x0) = 0 )

for f being PartFunc of REAL,REAL st ( f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0 ) & ( for r being Real st r < x0 holds

ex g being Real st

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

( f ^ is_left_convergent_in x0 & lim_left ((f ^),x0) = 0 )

proof end;

theorem :: LIMFUNC2:70

for x0 being Real

for f being PartFunc of REAL,REAL st ( f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) & ( for r being Real st x0 < r holds

ex g being Real st

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

( f ^ is_right_convergent_in x0 & lim_right ((f ^),x0) = 0 )

for f being PartFunc of REAL,REAL st ( f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) & ( for r being Real st x0 < r holds

ex g being Real st

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

( f ^ is_right_convergent_in x0 & lim_right ((f ^),x0) = 0 )

proof end;

theorem :: LIMFUNC2:71

for x0 being Real

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & lim_left (f,x0) = 0 & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds

0 < f . g ) ) holds

f ^ is_left_divergent_to+infty_in x0

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & lim_left (f,x0) = 0 & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds

0 < f . g ) ) holds

f ^ is_left_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC2:72

for x0 being Real

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & lim_left (f,x0) = 0 & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds

f . g < 0 ) ) holds

f ^ is_left_divergent_to-infty_in x0

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & lim_left (f,x0) = 0 & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds

f . g < 0 ) ) holds

f ^ is_left_divergent_to-infty_in x0

proof end;

theorem :: LIMFUNC2:73

for x0 being Real

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 & lim_right (f,x0) = 0 & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds

0 < f . g ) ) holds

f ^ is_right_divergent_to+infty_in x0

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 & lim_right (f,x0) = 0 & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds

0 < f . g ) ) holds

f ^ is_right_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC2:74

for x0 being Real

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 & lim_right (f,x0) = 0 & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds

f . g < 0 ) ) holds

f ^ is_right_divergent_to-infty_in x0

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 & lim_right (f,x0) = 0 & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds

f . g < 0 ) ) holds

f ^ is_right_divergent_to-infty_in x0

proof end;

theorem :: LIMFUNC2:75

for x0 being Real

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & lim_left (f,x0) = 0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f & f . g <> 0 ) ) & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds

0 <= f . g ) ) holds

f ^ is_left_divergent_to+infty_in x0

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & lim_left (f,x0) = 0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f & f . g <> 0 ) ) & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds

0 <= f . g ) ) holds

f ^ is_left_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC2:76

for x0 being Real

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & lim_left (f,x0) = 0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f & f . g <> 0 ) ) & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds

f . g <= 0 ) ) holds

f ^ is_left_divergent_to-infty_in x0

for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & lim_left (f,x0) = 0 & ( for r being Real st r < x0 holds

ex g being Real st

( r < g & g < x0 & g in dom f & f . g <> 0 ) ) & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds

f . g <= 0 ) ) holds

f ^ is_left_divergent_to-infty_in x0

proof end;

theorem :: LIMFUNC2:77

for x0 being Real

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 & lim_right (f,x0) = 0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f & f . g <> 0 ) ) & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds

0 <= f . g ) ) holds

f ^ is_right_divergent_to+infty_in x0

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 & lim_right (f,x0) = 0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f & f . g <> 0 ) ) & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds

0 <= f . g ) ) holds

f ^ is_right_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC2:78

for x0 being Real

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 & lim_right (f,x0) = 0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f & f . g <> 0 ) ) & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds

f . g <= 0 ) ) holds

f ^ is_right_divergent_to-infty_in x0

for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 & lim_right (f,x0) = 0 & ( for r being Real st x0 < r holds

ex g being Real st

( g < r & x0 < g & g in dom f & f . g <> 0 ) ) & ex r being Real st

( 0 < r & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds

f . g <= 0 ) ) holds

f ^ is_right_divergent_to-infty_in x0

proof end;