:: LIMFUNC3 semantic presentation

Lm1: for X, Y, Z being set st X c= Y \ Z holds
X c= Y

proof end;

Lm2: for g, r, r1 being real number st 0 < g & r <= r1 holds
( r - g < r1 & r < r1 + g )

proof end;

Lm3: for seq being Real_Sequence
for f1, f2 being PartFunc of REAL , REAL
for X being set st rng seq c= (dom (f1 (#) f2)) \ X holds
( rng seq c= dom (f1 (#) f2) & 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;

Lm4: for r being Real
for n being Nat holds
( r - (1 / (n + 1)) < r & r < r + (1 / (n + 1)) )

proof end;

Lm5: for n being Nat holds 0 < 1 / (n + 1)
by XREAL_1:141;

Lm6: for seq being Real_Sequence
for f1, f2 being PartFunc of REAL , REAL
for X being set st rng seq c= (dom (f1 + f2)) \ X holds
( rng seq c= dom (f1 + f2) & 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;

theorem Th1: :: LIMFUNC3:1

for x0 being Real
for seq being Real_Sequence
for f being PartFunc of REAL , REAL st ( rng seq c= (dom f) /\ (left_open_halfline x0) or rng seq c= (dom f) /\ (right_open_halfline x0) ) holds
rng seq c= (dom f) \ {x0}

proof end;

theorem Th2: :: LIMFUNC3:2

for x0 being Real
for seq being Real_Sequence
for f being PartFunc of REAL , REAL st ( for n being Nat holds
( 0 < abs (x0 - (seq . n)) & abs (x0 - (seq . n)) < 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) \ {x0} )

proof end;

theorem Th3: :: LIMFUNC3:3

for x0 being Real
for seq being Real_Sequence
for f being PartFunc of REAL , REAL st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds
for r being Real st 0 < r holds
ex n being Nat st
for k being Nat st n <= k holds
( 0 < abs (x0 - (seq . k)) & abs (x0 - (seq . k)) < r & seq . k in dom f )

proof end;

theorem Th4: :: LIMFUNC3:4

for r, x0 being Real st 0 < r holds
].(x0 - r),(x0 + r).[ \ {x0} = ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[

proof end;

theorem Th5: :: LIMFUNC3:5

for r2, x0 being Real
for f being PartFunc of REAL , REAL st 0 < r2 & ].(x0 - r2),x0.[ \/ ].x0,(x0 + r2).[ c= dom f holds
for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )

proof end;

theorem Th6: :: LIMFUNC3:6

for x0 being Real
for seq being Real_Sequence
for f being PartFunc of REAL , REAL st ( for n being 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) \ {x0} )

proof end;

theorem Th7: :: LIMFUNC3:7

for x0, g being Real
for seq being Real_Sequence st seq is convergent & lim seq = x0 & 0 < g holds
ex k being Nat st
for n being Nat st k <= n holds
( x0 - g < seq . n & seq . n < x0 + g )

proof end;

theorem Th8: :: LIMFUNC3:8

for x0 being Real
for f being PartFunc of REAL , REAL holds
( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) iff ( ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) ) )

proof end;

definition

let f be PartFunc of REAL , REAL ;
let x0 be Real;
pred f is_convergent_in x0 means :Def1: :: LIMFUNC3:def 1
( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 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) \ {x0} holds
( f * seq is convergent & lim (f * seq) = g ) );
pred f is_divergent_to+infty_in x0 means :Def2: :: LIMFUNC3:def 2
( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds
f * seq is divergent_to+infty ) );
pred f is_divergent_to-infty_in x0 means :Def3: :: LIMFUNC3:def 3
( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds
f * seq is divergent_to-infty ) );

end;

:: deftheorem Def1 defines is_convergent_in LIMFUNC3:def 1 :

:: deftheorem Def2 defines is_divergent_to+infty_in LIMFUNC3:def 2 :

:: deftheorem Def3 defines is_divergent_to-infty_in LIMFUNC3:def 3 :

theorem :: LIMFUNC3:9

canceled;

theorem :: LIMFUNC3:10

canceled;

theorem :: LIMFUNC3:11

canceled;

theorem :: LIMFUNC3:12

for x0 being Real
for f being PartFunc of REAL , REAL holds
( f is_convergent_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f holds
abs ((f . r1) - g) < g1 ) ) ) )

proof end;

theorem :: LIMFUNC3:13

for x0 being Real
for f being PartFunc of REAL , REAL holds
( f is_divergent_to+infty_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for g1 being Real ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f holds
g1 < f . r1 ) ) ) ) )

proof end;

theorem :: LIMFUNC3:14

for x0 being Real
for f being PartFunc of REAL , REAL holds
( f is_divergent_to-infty_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for g1 being Real ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f holds
f . r1 < g1 ) ) ) ) )

proof end;

theorem Th15: :: LIMFUNC3:15

for x0 being Real
for f being PartFunc of REAL , REAL holds
( f is_divergent_to+infty_in x0 iff ( f is_left_divergent_to+infty_in x0 & f is_right_divergent_to+infty_in x0 ) )

proof end;

theorem Th16: :: LIMFUNC3:16

for x0 being Real
for f being PartFunc of REAL , REAL holds
( f is_divergent_to-infty_in x0 iff ( f is_left_divergent_to-infty_in x0 & f is_right_divergent_to-infty_in x0 ) )

proof end;

theorem :: LIMFUNC3:17

for x0 being Real
for f1, f2 being PartFunc of REAL , REAL st f1 is_divergent_to+infty_in x0 & f2 is_divergent_to+infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in (dom f1) /\ (dom f2) & g2 < r2 & x0 < g2 & g2 in (dom f1) /\ (dom f2) ) ) holds
( f1 + f2 is_divergent_to+infty_in x0 & f1 (#) f2 is_divergent_to+infty_in x0 )

proof end;

theorem :: LIMFUNC3:18

for x0 being Real
for f1, f2 being PartFunc of REAL , REAL st f1 is_divergent_to-infty_in x0 & f2 is_divergent_to-infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in (dom f1) /\ (dom f2) & g2 < r2 & x0 < g2 & g2 in (dom f1) /\ (dom f2) ) ) holds
( f1 + f2 is_divergent_to-infty_in x0 & f1 (#) f2 is_divergent_to+infty_in x0 )

proof end;

theorem :: LIMFUNC3:19

for x0 being Real
for f1, f2 being PartFunc of REAL , REAL st f1 is_divergent_to+infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 + f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 + f2) ) ) & ex r being Real st
( 0 < r & f2 is_bounded_below_on ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ ) holds
f1 + f2 is_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC3:20

for x0 being Real
for f1, f2 being PartFunc of REAL , REAL st f1 is_divergent_to+infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 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.[ \/ ].x0,(x0 + r).[) holds
r1 <= f2 . g ) ) holds
f1 (#) f2 is_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC3:21

for x0, r being Real
for f being PartFunc of REAL , REAL holds
( ( f is_divergent_to+infty_in x0 & r > 0 implies r (#) f is_divergent_to+infty_in x0 ) & ( f is_divergent_to+infty_in x0 & r < 0 implies r (#) f is_divergent_to-infty_in x0 ) & ( f is_divergent_to-infty_in x0 & r > 0 implies r (#) f is_divergent_to-infty_in x0 ) & ( f is_divergent_to-infty_in x0 & r < 0 implies r (#) f is_divergent_to+infty_in x0 ) )

proof end;

theorem :: LIMFUNC3:22

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

proof end;

theorem Th23: :: LIMFUNC3:23

for x0 being Real
for f being PartFunc of REAL , REAL st ex r being Real st
( 0 < r & f is_non_decreasing_on ].(x0 - r),x0.[ & f is_non_increasing_on ].x0,(x0 + r).[ & not f is_bounded_above_on ].(x0 - r),x0.[ & not f is_bounded_above_on ].x0,(x0 + r).[ ) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) holds
f is_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC3:24

for x0 being Real
for f being PartFunc of REAL , REAL st ex r being Real st
( 0 < r & f is_increasing_on ].(x0 - r),x0.[ & f is_decreasing_on ].x0,(x0 + r).[ & not f is_bounded_above_on ].(x0 - r),x0.[ & not f is_bounded_above_on ].x0,(x0 + r).[ ) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) holds
f is_divergent_to+infty_in x0

proof end;

theorem Th25: :: LIMFUNC3:25

for x0 being Real
for f being PartFunc of REAL , REAL st ex r being Real st
( 0 < r & f is_non_increasing_on ].(x0 - r),x0.[ & f is_non_decreasing_on ].x0,(x0 + r).[ & not f is_bounded_below_on ].(x0 - r),x0.[ & not f is_bounded_below_on ].x0,(x0 + r).[ ) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) holds
f is_divergent_to-infty_in x0

proof end;

theorem :: LIMFUNC3:26

for x0 being Real
for f being PartFunc of REAL , REAL st ex r being Real st
( 0 < r & f is_decreasing_on ].(x0 - r),x0.[ & f is_increasing_on ].x0,(x0 + r).[ & not f is_bounded_below_on ].(x0 - r),x0.[ & not f is_bounded_below_on ].x0,(x0 + r).[ ) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) holds
f is_divergent_to-infty_in x0

proof end;

theorem Th27: :: LIMFUNC3:27

for x0 being Real
for f1, f being PartFunc of REAL , REAL st f1 is_divergent_to+infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex r being Real st
( 0 < r & (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f1 . g <= f . g ) ) holds
f is_divergent_to+infty_in x0

proof end;

theorem Th28: :: LIMFUNC3:28

for x0 being Real
for f1, f being PartFunc of REAL , REAL st f1 is_divergent_to-infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex r being Real st
( 0 < r & (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f . g <= f1 . g ) ) holds
f is_divergent_to-infty_in x0

proof end;

theorem :: LIMFUNC3:29

for x0 being Real
for f1, f being PartFunc of REAL , REAL st f1 is_divergent_to+infty_in x0 & ex r being Real st
( 0 < r & ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ holds
f1 . g <= f . g ) ) holds
f is_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC3:30

for x0 being Real
for f1, f being PartFunc of REAL , REAL st f1 is_divergent_to-infty_in x0 & ex r being Real st
( 0 < r & ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ holds
f . g <= f1 . g ) ) holds
f is_divergent_to-infty_in x0

proof end;

definition

let f be PartFunc of REAL , REAL ;
let x0 be Real;
assume A1: f is_convergent_in x0 ;
func lim f,x0 -> Real means :Def4: :: LIMFUNC3:def 4
for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds
( f * seq is convergent & lim (f * seq) = it );
existence by A1, Def1;
uniqueness

proof end;

end;

:: deftheorem Def4 defines lim LIMFUNC3:def 4 :

theorem :: LIMFUNC3:31

canceled;

theorem :: LIMFUNC3:32

for x0, g being Real
for f being PartFunc of REAL , REAL st f is_convergent_in x0 holds
( lim f,x0 = g iff for g1 being Real st 0 < g1 holds
ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < abs (x0 - r1) & abs (x0 - r1) < g2 & r1 in dom f holds
abs ((f . r1) - g) < g1 ) ) )

proof end;

theorem Th33: :: LIMFUNC3:33

for x0 being Real
for f being PartFunc of REAL , REAL st f is_convergent_in x0 holds
( f is_left_convergent_in x0 & f is_right_convergent_in x0 & lim_left f,x0 = lim_right f,x0 & lim f,x0 = lim_left f,x0 & lim f,x0 = lim_right f,x0 )

proof end;

theorem :: LIMFUNC3:34

for x0 being Real
for f being PartFunc of REAL , REAL st f is_left_convergent_in x0 & f is_right_convergent_in x0 & lim_left f,x0 = lim_right f,x0 holds
( f is_convergent_in x0 & lim f,x0 = lim_left f,x0 & lim f,x0 = lim_right f,x0 )

proof end;

theorem Th35: :: LIMFUNC3:35

for x0, r being Real
for f being PartFunc of REAL , REAL st f is_convergent_in x0 holds
( r (#) f is_convergent_in x0 & lim (r (#) f),x0 = r * (lim f,x0) )

proof end;

theorem Th36: :: LIMFUNC3:36

for x0 being Real
for f being PartFunc of REAL , REAL st f is_convergent_in x0 holds
( - f is_convergent_in x0 & lim (- f),x0 = - (lim f,x0) )

proof end;

theorem Th37: :: LIMFUNC3:37

for x0 being Real
for f1, f2 being PartFunc of REAL , REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 + f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 + f2) ) ) holds
( f1 + f2 is_convergent_in x0 & lim (f1 + f2),x0 = (lim f1,x0) + (lim f2,x0) )

proof end;

theorem :: LIMFUNC3:38

for x0 being Real
for f1, f2 being PartFunc of REAL , REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 - f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 - f2) ) ) holds
( f1 - f2 is_convergent_in x0 & lim (f1 - f2),x0 = (lim f1,x0) - (lim f2,x0) )

proof end;

theorem :: LIMFUNC3:39

for x0 being Real
for f being PartFunc of REAL , REAL st f is_convergent_in x0 & f " {0} = {} & lim f,x0 <> 0 holds
( f ^ is_convergent_in x0 & lim (f ^ ),x0 = (lim f,x0) " )

proof end;

theorem :: LIMFUNC3:40

for x0 being Real
for f being PartFunc of REAL , REAL st f is_convergent_in x0 holds
( abs f is_convergent_in x0 & lim (abs f),x0 = abs (lim f,x0) )

proof end;

theorem Th41: :: LIMFUNC3:41

for x0 being Real
for f being PartFunc of REAL , REAL st f is_convergent_in x0 & lim f,x0 <> 0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f & f . g1 <> 0 & f . g2 <> 0 ) ) holds
( f ^ is_convergent_in x0 & lim (f ^ ),x0 = (lim f,x0) " )

proof end;

theorem Th42: :: LIMFUNC3:42

for x0 being Real
for f1, f2 being PartFunc of REAL , REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 (#) f2) ) ) holds
( f1 (#) f2 is_convergent_in x0 & lim (f1 (#) f2),x0 = (lim f1,x0) * (lim f2,x0) )

proof end;

theorem :: LIMFUNC3:43

for x0 being Real
for f1, f2 being PartFunc of REAL , REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim f2,x0 <> 0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 / f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 / f2) ) ) holds
( f1 / f2 is_convergent_in x0 & lim (f1 / f2),x0 = (lim f1,x0) / (lim f2,x0) )

proof end;

theorem :: LIMFUNC3:44

for x0 being Real
for f1, f2 being PartFunc of REAL , REAL st f1 is_convergent_in x0 & lim f1,x0 = 0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 (#) f2) ) ) & ex r being Real st
( 0 < r & f2 is_bounded_on ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ ) holds
( f1 (#) f2 is_convergent_in x0 & lim (f1 (#) f2),x0 = 0 )

proof end;

theorem Th45: :: LIMFUNC3:45

for x0 being Real
for f1, f2, f being PartFunc of REAL , REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim f1,x0 = lim f2,x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
( f1 . g <= f . g & f . g <= f2 . g ) ) & ( ( (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) ) or ( (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) ) ) ) holds
( f is_convergent_in x0 & lim f,x0 = lim f1,x0 )

proof end;

theorem :: LIMFUNC3:46

for x0 being Real
for f1, f2, f being PartFunc of REAL , REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim f1,x0 = lim f2,x0 & ex r being Real st
( 0 < r & ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is_convergent_in x0 & lim f,x0 = lim f1,x0 )

proof end;

theorem :: LIMFUNC3:47

for x0 being Real
for f1, f2 being PartFunc of REAL , REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & ex r being Real st
( 0 < r & ( ( (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & ( for g being Real st g in (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & ( for g being Real st g in (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f1 . g <= f2 . g ) ) ) ) holds
lim f1,x0 <= lim f2,x0

proof end;

theorem :: LIMFUNC3:48

for x0 being Real
for f being PartFunc of REAL , REAL st ( f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0 ) & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f & f . g1 <> 0 & f . g2 <> 0 ) ) holds
( f ^ is_convergent_in x0 & lim (f ^ ),x0 = 0 )

proof end;

theorem :: LIMFUNC3:49

for x0 being Real
for f being PartFunc of REAL , REAL st f is_convergent_in x0 & lim f,x0 = 0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f & f . g1 <> 0 & f . g2 <> 0 ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
0 <= f . g ) ) holds
f ^ is_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC3:50

for x0 being Real
for f being PartFunc of REAL , REAL st f is_convergent_in x0 & lim f,x0 = 0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f & f . g1 <> 0 & f . g2 <> 0 ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f . g <= 0 ) ) holds
f ^ is_divergent_to-infty_in x0

proof end;

theorem :: LIMFUNC3:51

for x0 being Real
for f being PartFunc of REAL , REAL st f is_convergent_in x0 & lim f,x0 = 0 & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
0 < f . g ) ) holds
f ^ is_divergent_to+infty_in x0

proof end;

theorem :: LIMFUNC3:52

for x0 being Real
for f being PartFunc of REAL , REAL st f is_convergent_in x0 & lim f,x0 = 0 & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f . g < 0 ) ) holds
f ^ is_divergent_to-infty_in x0

proof end;