:: LIMFUNC3 semantic presentation

Lemma1: for b1, b2, b3 being set st b1 c= b2 \ b3 holds
b1 c= b2
proof end;

Lemma2: for b1, b2, b3 being real number st 0 < b1 & b2 <= b3 holds
( b2 - b1 < b3 & b2 < b3 + b1 )
proof end;

Lemma3: for b1 being Real_Sequence
for b2, b3 being PartFunc of REAL , REAL
for b4 being set st rng b1 c= (dom (b2 (#) b3)) \ b4 holds
( rng b1 c= dom (b2 (#) b3) & dom (b2 (#) b3) = (dom b2) /\ (dom b3) & rng b1 c= dom b2 & rng b1 c= dom b3 & rng b1 c= (dom b2) \ b4 & rng b1 c= (dom b3) \ b4 )
proof end;

Lemma4: for b1 being Real
for b2 being Nat holds
( b1 - (1 / (b2 + 1)) < b1 & b1 < b1 + (1 / (b2 + 1)) )
proof end;

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

Lemma6: for b1 being Real_Sequence
for b2, b3 being PartFunc of REAL , REAL
for b4 being set st rng b1 c= (dom (b2 + b3)) \ b4 holds
( rng b1 c= dom (b2 + b3) & dom (b2 + b3) = (dom b2) /\ (dom b3) & rng b1 c= dom b2 & rng b1 c= dom b3 & rng b1 c= (dom b2) \ b4 & rng b1 c= (dom b3) \ b4 )
proof end;

theorem Th1: :: LIMFUNC3:1
for b1 being Real
for b2 being Real_Sequence
for b3 being PartFunc of REAL , REAL st ( rng b2 c= (dom b3) /\ (left_open_halfline b1) or rng b2 c= (dom b3) /\ (right_open_halfline b1) ) holds
rng b2 c= (dom b3) \ {b1}
proof end;

theorem Th2: :: LIMFUNC3:2
for b1 being Real
for b2 being Real_Sequence
for b3 being PartFunc of REAL , REAL st ( for b4 being Nat holds
( 0 < abs (b1 - (b2 . b4)) & abs (b1 - (b2 . b4)) < 1 / (b4 + 1) & b2 . b4 in dom b3 ) ) holds
( b2 is convergent & lim b2 = b1 & rng b2 c= dom b3 & rng b2 c= (dom b3) \ {b1} )
proof end;

theorem Th3: :: LIMFUNC3:3
for b1 being Real
for b2 being Real_Sequence
for b3 being PartFunc of REAL , REAL st b2 is convergent & lim b2 = b1 & rng b2 c= (dom b3) \ {b1} holds
for b4 being Real st 0 < b4 holds
ex b5 being Nat st
for b6 being Nat st b5 <= b6 holds
( 0 < abs (b1 - (b2 . b6)) & abs (b1 - (b2 . b6)) < b4 & b2 . b6 in dom b3 )
proof end;

theorem Th4: :: LIMFUNC3:4
for b1, b2 being Real st 0 < b1 holds
].(b2 - b1),(b2 + b1).[ \ {b2} = ].(b2 - b1),b2.[ \/ ].b2,(b2 + b1).[
proof end;

theorem Th5: :: LIMFUNC3:5
for b1, b2 being Real
for b3 being PartFunc of REAL , REAL st 0 < b1 & ].(b2 - b1),b2.[ \/ ].b2,(b2 + b1).[ c= dom b3 holds
for b4, b5 being Real st b4 < b2 & b2 < b5 holds
ex b6, b7 being Real st
( b4 < b6 & b6 < b2 & b6 in dom b3 & b7 < b5 & b2 < b7 & b7 in dom b3 )
proof end;

theorem Th6: :: LIMFUNC3:6
for b1 being Real
for b2 being Real_Sequence
for b3 being PartFunc of REAL , REAL st ( for b4 being Nat holds
( b1 - (1 / (b4 + 1)) < b2 . b4 & b2 . b4 < b1 & b2 . b4 in dom b3 ) ) holds
( b2 is convergent & lim b2 = b1 & rng b2 c= (dom b3) \ {b1} )
proof end;

theorem Th7: :: LIMFUNC3:7
for b1, b2 being Real
for b3 being Real_Sequence st b3 is convergent & lim b3 = b1 & 0 < b2 holds
ex b4 being Nat st
for b5 being Nat st b4 <= b5 holds
( b1 - b2 < b3 . b5 & b3 . b5 < b1 + b2 )
proof end;

theorem Th8: :: LIMFUNC3:8
for b1 being Real
for b2 being PartFunc of REAL , REAL holds
( ( for b3, b4 being Real st b3 < b1 & b1 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b1 & b5 in dom b2 & b6 < b4 & b1 < b6 & b6 in dom b2 ) ) iff ( ( for b3 being Real st b3 < b1 holds
ex b4 being Real st
( b3 < b4 & b4 < b1 & b4 in dom b2 ) ) & ( for b3 being Real st b1 < b3 holds
ex b4 being Real st
( b4 < b3 & b1 < b4 & b4 in dom b2 ) ) ) )
proof end;

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be Real;
pred c1 is_convergent_in c2 means :Def1: :: LIMFUNC3:def 1
( ( for b1, b2 being Real st b1 < a2 & a2 < b2 holds
ex b3, b4 being Real st
( b1 < b3 & b3 < a2 & b3 in dom a1 & b4 < b2 & a2 < b4 & b4 in dom a1 ) ) & ex b1 being Real st
for b2 being Real_Sequence st b2 is convergent & lim b2 = a2 & rng b2 c= (dom a1) \ {a2} holds
( a1 * b2 is convergent & lim (a1 * b2) = b1 ) );
pred c1 is_divergent_to+infty_in c2 means :Def2: :: LIMFUNC3:def 2
( ( for b1, b2 being Real st b1 < a2 & a2 < b2 holds
ex b3, b4 being Real st
( b1 < b3 & b3 < a2 & b3 in dom a1 & b4 < b2 & a2 < b4 & b4 in dom a1 ) ) & ( for b1 being Real_Sequence st b1 is convergent & lim b1 = a2 & rng b1 c= (dom a1) \ {a2} holds
a1 * b1 is divergent_to+infty ) );
pred c1 is_divergent_to-infty_in c2 means :Def3: :: LIMFUNC3:def 3
( ( for b1, b2 being Real st b1 < a2 & a2 < b2 holds
ex b3, b4 being Real st
( b1 < b3 & b3 < a2 & b3 in dom a1 & b4 < b2 & a2 < b4 & b4 in dom a1 ) ) & ( for b1 being Real_Sequence st b1 is convergent & lim b1 = a2 & rng b1 c= (dom a1) \ {a2} holds
a1 * b1 is divergent_to-infty ) );
end;

:: deftheorem Def1 defines is_convergent_in LIMFUNC3:def 1 :
for b1 being PartFunc of REAL , REAL
for b2 being Real holds
( b1 is_convergent_in b2 iff ( ( for b3, b4 being Real st b3 < b2 & b2 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b2 & b5 in dom b1 & b6 < b4 & b2 < b6 & b6 in dom b1 ) ) & ex b3 being Real st
for b4 being Real_Sequence st b4 is convergent & lim b4 = b2 & rng b4 c= (dom b1) \ {b2} holds
( b1 * b4 is convergent & lim (b1 * b4) = b3 ) ) );

:: deftheorem Def2 defines is_divergent_to+infty_in LIMFUNC3:def 2 :
for b1 being PartFunc of REAL , REAL
for b2 being Real holds
( b1 is_divergent_to+infty_in b2 iff ( ( for b3, b4 being Real st b3 < b2 & b2 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b2 & b5 in dom b1 & b6 < b4 & b2 < b6 & b6 in dom b1 ) ) & ( for b3 being Real_Sequence st b3 is convergent & lim b3 = b2 & rng b3 c= (dom b1) \ {b2} holds
b1 * b3 is divergent_to+infty ) ) );

:: deftheorem Def3 defines is_divergent_to-infty_in LIMFUNC3:def 3 :
for b1 being PartFunc of REAL , REAL
for b2 being Real holds
( b1 is_divergent_to-infty_in b2 iff ( ( for b3, b4 being Real st b3 < b2 & b2 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b2 & b5 in dom b1 & b6 < b4 & b2 < b6 & b6 in dom b1 ) ) & ( for b3 being Real_Sequence st b3 is convergent & lim b3 = b2 & rng b3 c= (dom b1) \ {b2} holds
b1 * b3 is divergent_to-infty ) ) );

theorem Th9: :: LIMFUNC3:9
canceled;

theorem Th10: :: LIMFUNC3:10
canceled;

theorem Th11: :: LIMFUNC3:11
canceled;

theorem Th12: :: LIMFUNC3:12
for b1 being Real
for b2 being PartFunc of REAL , REAL holds
( b2 is_convergent_in b1 iff ( ( for b3, b4 being Real st b3 < b1 & b1 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b1 & b5 in dom b2 & b6 < b4 & b1 < b6 & b6 in dom b2 ) ) & ex b3 being Real st
for b4 being Real st 0 < b4 holds
ex b5 being Real st
( 0 < b5 & ( for b6 being Real st 0 < abs (b1 - b6) & abs (b1 - b6) < b5 & b6 in dom b2 holds
abs ((b2 . b6) - b3) < b4 ) ) ) )
proof end;

theorem Th13: :: LIMFUNC3:13
for b1 being Real
for b2 being PartFunc of REAL , REAL holds
( b2 is_divergent_to+infty_in b1 iff ( ( for b3, b4 being Real st b3 < b1 & b1 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b1 & b5 in dom b2 & b6 < b4 & b1 < b6 & b6 in dom b2 ) ) & ( for b3 being Real ex b4 being Real st
( 0 < b4 & ( for b5 being Real st 0 < abs (b1 - b5) & abs (b1 - b5) < b4 & b5 in dom b2 holds
b3 < b2 . b5 ) ) ) ) )
proof end;

theorem Th14: :: LIMFUNC3:14
for b1 being Real
for b2 being PartFunc of REAL , REAL holds
( b2 is_divergent_to-infty_in b1 iff ( ( for b3, b4 being Real st b3 < b1 & b1 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b1 & b5 in dom b2 & b6 < b4 & b1 < b6 & b6 in dom b2 ) ) & ( for b3 being Real ex b4 being Real st
( 0 < b4 & ( for b5 being Real st 0 < abs (b1 - b5) & abs (b1 - b5) < b4 & b5 in dom b2 holds
b2 . b5 < b3 ) ) ) ) )
proof end;

theorem Th15: :: LIMFUNC3:15
for b1 being Real
for b2 being PartFunc of REAL , REAL holds
( b2 is_divergent_to+infty_in b1 iff ( b2 is_left_divergent_to+infty_in b1 & b2 is_right_divergent_to+infty_in b1 ) )
proof end;

theorem Th16: :: LIMFUNC3:16
for b1 being Real
for b2 being PartFunc of REAL , REAL holds
( b2 is_divergent_to-infty_in b1 iff ( b2 is_left_divergent_to-infty_in b1 & b2 is_right_divergent_to-infty_in b1 ) )
proof end;

theorem Th17: :: LIMFUNC3:17
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_divergent_to+infty_in b1 & b3 is_divergent_to+infty_in b1 & ( for b4, b5 being Real st b4 < b1 & b1 < b5 holds
ex b6, b7 being Real st
( b4 < b6 & b6 < b1 & b6 in (dom b2) /\ (dom b3) & b7 < b5 & b1 < b7 & b7 in (dom b2) /\ (dom b3) ) ) holds
( b2 + b3 is_divergent_to+infty_in b1 & b2 (#) b3 is_divergent_to+infty_in b1 )
proof end;

theorem Th18: :: LIMFUNC3:18
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_divergent_to-infty_in b1 & b3 is_divergent_to-infty_in b1 & ( for b4, b5 being Real st b4 < b1 & b1 < b5 holds
ex b6, b7 being Real st
( b4 < b6 & b6 < b1 & b6 in (dom b2) /\ (dom b3) & b7 < b5 & b1 < b7 & b7 in (dom b2) /\ (dom b3) ) ) holds
( b2 + b3 is_divergent_to-infty_in b1 & b2 (#) b3 is_divergent_to+infty_in b1 )
proof end;

theorem Th19: :: LIMFUNC3:19
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_divergent_to+infty_in b1 & ( for b4, b5 being Real st b4 < b1 & b1 < b5 holds
ex b6, b7 being Real st
( b4 < b6 & b6 < b1 & b6 in dom (b2 + b3) & b7 < b5 & b1 < b7 & b7 in dom (b2 + b3) ) ) & ex b4 being Real st
( 0 < b4 & b3 is_bounded_below_on ].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[ ) holds
b2 + b3 is_divergent_to+infty_in b1
proof end;

theorem Th20: :: LIMFUNC3:20
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_divergent_to+infty_in b1 & ( for b4, b5 being Real st b4 < b1 & b1 < b5 holds
ex b6, b7 being Real st
( b4 < b6 & b6 < b1 & b6 in dom (b2 (#) b3) & b7 < b5 & b1 < b7 & b7 in dom (b2 (#) b3) ) ) & ex b4, b5 being Real st
( 0 < b4 & 0 < b5 & ( for b6 being Real st b6 in (dom b3) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) holds
b5 <= b3 . b6 ) ) holds
b2 (#) b3 is_divergent_to+infty_in b1
proof end;

theorem Th21: :: LIMFUNC3:21
for b1, b2 being Real
for b3 being PartFunc of REAL , REAL holds
( ( b3 is_divergent_to+infty_in b1 & b2 > 0 implies b2 (#) b3 is_divergent_to+infty_in b1 ) & ( b3 is_divergent_to+infty_in b1 & b2 < 0 implies b2 (#) b3 is_divergent_to-infty_in b1 ) & ( b3 is_divergent_to-infty_in b1 & b2 > 0 implies b2 (#) b3 is_divergent_to-infty_in b1 ) & ( b3 is_divergent_to-infty_in b1 & b2 < 0 implies b2 (#) b3 is_divergent_to+infty_in b1 ) )
proof end;

theorem Th22: :: LIMFUNC3:22
for b1 being Real
for b2 being PartFunc of REAL , REAL st ( b2 is_divergent_to+infty_in b1 or b2 is_divergent_to-infty_in b1 ) holds
abs b2 is_divergent_to+infty_in b1
proof end;

theorem Th23: :: LIMFUNC3:23
for b1 being Real
for b2 being PartFunc of REAL , REAL st ex b3 being Real st
( 0 < b3 & b2 is_non_decreasing_on ].(b1 - b3),b1.[ & b2 is_non_increasing_on ].b1,(b1 + b3).[ & not b2 is_bounded_above_on ].(b1 - b3),b1.[ & not b2 is_bounded_above_on ].b1,(b1 + b3).[ ) & ( for b3, b4 being Real st b3 < b1 & b1 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b1 & b5 in dom b2 & b6 < b4 & b1 < b6 & b6 in dom b2 ) ) holds
b2 is_divergent_to+infty_in b1
proof end;

theorem Th24: :: LIMFUNC3:24
for b1 being Real
for b2 being PartFunc of REAL , REAL st ex b3 being Real st
( 0 < b3 & b2 is_increasing_on ].(b1 - b3),b1.[ & b2 is_decreasing_on ].b1,(b1 + b3).[ & not b2 is_bounded_above_on ].(b1 - b3),b1.[ & not b2 is_bounded_above_on ].b1,(b1 + b3).[ ) & ( for b3, b4 being Real st b3 < b1 & b1 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b1 & b5 in dom b2 & b6 < b4 & b1 < b6 & b6 in dom b2 ) ) holds
b2 is_divergent_to+infty_in b1
proof end;

theorem Th25: :: LIMFUNC3:25
for b1 being Real
for b2 being PartFunc of REAL , REAL st ex b3 being Real st
( 0 < b3 & b2 is_non_increasing_on ].(b1 - b3),b1.[ & b2 is_non_decreasing_on ].b1,(b1 + b3).[ & not b2 is_bounded_below_on ].(b1 - b3),b1.[ & not b2 is_bounded_below_on ].b1,(b1 + b3).[ ) & ( for b3, b4 being Real st b3 < b1 & b1 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b1 & b5 in dom b2 & b6 < b4 & b1 < b6 & b6 in dom b2 ) ) holds
b2 is_divergent_to-infty_in b1
proof end;

theorem Th26: :: LIMFUNC3:26
for b1 being Real
for b2 being PartFunc of REAL , REAL st ex b3 being Real st
( 0 < b3 & b2 is_decreasing_on ].(b1 - b3),b1.[ & b2 is_increasing_on ].b1,(b1 + b3).[ & not b2 is_bounded_below_on ].(b1 - b3),b1.[ & not b2 is_bounded_below_on ].b1,(b1 + b3).[ ) & ( for b3, b4 being Real st b3 < b1 & b1 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b1 & b5 in dom b2 & b6 < b4 & b1 < b6 & b6 in dom b2 ) ) holds
b2 is_divergent_to-infty_in b1
proof end;

theorem Th27: :: LIMFUNC3:27
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_divergent_to+infty_in b1 & ( for b4, b5 being Real st b4 < b1 & b1 < b5 holds
ex b6, b7 being Real st
( b4 < b6 & b6 < b1 & b6 in dom b3 & b7 < b5 & b1 < b7 & b7 in dom b3 ) ) & ex b4 being Real st
( 0 < b4 & (dom b3) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) c= (dom b2) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) & ( for b5 being Real st b5 in (dom b3) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) holds
b2 . b5 <= b3 . b5 ) ) holds
b3 is_divergent_to+infty_in b1
proof end;

theorem Th28: :: LIMFUNC3:28
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_divergent_to-infty_in b1 & ( for b4, b5 being Real st b4 < b1 & b1 < b5 holds
ex b6, b7 being Real st
( b4 < b6 & b6 < b1 & b6 in dom b3 & b7 < b5 & b1 < b7 & b7 in dom b3 ) ) & ex b4 being Real st
( 0 < b4 & (dom b3) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) c= (dom b2) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) & ( for b5 being Real st b5 in (dom b3) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) holds
b3 . b5 <= b2 . b5 ) ) holds
b3 is_divergent_to-infty_in b1
proof end;

theorem Th29: :: LIMFUNC3:29
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_divergent_to+infty_in b1 & ex b4 being Real st
( 0 < b4 & ].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[ c= (dom b3) /\ (dom b2) & ( for b5 being Real st b5 in ].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[ holds
b2 . b5 <= b3 . b5 ) ) holds
b3 is_divergent_to+infty_in b1
proof end;

theorem Th30: :: LIMFUNC3:30
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_divergent_to-infty_in b1 & ex b4 being Real st
( 0 < b4 & ].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[ c= (dom b3) /\ (dom b2) & ( for b5 being Real st b5 in ].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[ holds
b3 . b5 <= b2 . b5 ) ) holds
b3 is_divergent_to-infty_in b1
proof end;

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be Real;
assume E24: c1 is_convergent_in c2 ;
func lim c1,c2 -> Real means :Def4: :: LIMFUNC3:def 4
for b1 being Real_Sequence st b1 is convergent & lim b1 = a2 & rng b1 c= (dom a1) \ {a2} holds
( a1 * b1 is convergent & lim (a1 * b1) = a3 );
existence
ex b1 being Real st
for b2 being Real_Sequence st b2 is convergent & lim b2 = c2 & rng b2 c= (dom c1) \ {c2} holds
( c1 * b2 is convergent & lim (c1 * b2) = b1 ) by E24, Def1;
uniqueness
for b1, b2 being Real st ( for b3 being Real_Sequence st b3 is convergent & lim b3 = c2 & rng b3 c= (dom c1) \ {c2} holds
( c1 * b3 is convergent & lim (c1 * b3) = b1 ) ) & ( for b3 being Real_Sequence st b3 is convergent & lim b3 = c2 & rng b3 c= (dom c1) \ {c2} holds
( c1 * b3 is convergent & lim (c1 * b3) = b2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines lim LIMFUNC3:def 4 :
for b1 being PartFunc of REAL , REAL
for b2 being Real st b1 is_convergent_in b2 holds
for b3 being Real holds
( b3 = lim b1,b2 iff for b4 being Real_Sequence st b4 is convergent & lim b4 = b2 & rng b4 c= (dom b1) \ {b2} holds
( b1 * b4 is convergent & lim (b1 * b4) = b3 ) );

theorem Th31: :: LIMFUNC3:31
canceled;

theorem Th32: :: LIMFUNC3:32
for b1, b2 being Real
for b3 being PartFunc of REAL , REAL st b3 is_convergent_in b1 holds
( lim b3,b1 = b2 iff for b4 being Real st 0 < b4 holds
ex b5 being Real st
( 0 < b5 & ( for b6 being Real st 0 < abs (b1 - b6) & abs (b1 - b6) < b5 & b6 in dom b3 holds
abs ((b3 . b6) - b2) < b4 ) ) )
proof end;

theorem Th33: :: LIMFUNC3:33
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_convergent_in b1 holds
( b2 is_left_convergent_in b1 & b2 is_right_convergent_in b1 & lim_left b2,b1 = lim_right b2,b1 & lim b2,b1 = lim_left b2,b1 & lim b2,b1 = lim_right b2,b1 )
proof end;

theorem Th34: :: LIMFUNC3:34
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_left_convergent_in b1 & b2 is_right_convergent_in b1 & lim_left b2,b1 = lim_right b2,b1 holds
( b2 is_convergent_in b1 & lim b2,b1 = lim_left b2,b1 & lim b2,b1 = lim_right b2,b1 )
proof end;

theorem Th35: :: LIMFUNC3:35
for b1, b2 being Real
for b3 being PartFunc of REAL , REAL st b3 is_convergent_in b1 holds
( b2 (#) b3 is_convergent_in b1 & lim (b2 (#) b3),b1 = b2 * (lim b3,b1) )
proof end;

theorem Th36: :: LIMFUNC3:36
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_convergent_in b1 holds
( - b2 is_convergent_in b1 & lim (- b2),b1 = - (lim b2,b1) )
proof end;

theorem Th37: :: LIMFUNC3:37
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_convergent_in b1 & ( for b4, b5 being Real st b4 < b1 & b1 < b5 holds
ex b6, b7 being Real st
( b4 < b6 & b6 < b1 & b6 in dom (b2 + b3) & b7 < b5 & b1 < b7 & b7 in dom (b2 + b3) ) ) holds
( b2 + b3 is_convergent_in b1 & lim (b2 + b3),b1 = (lim b2,b1) + (lim b3,b1) )
proof end;

theorem Th38: :: LIMFUNC3:38
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_convergent_in b1 & ( for b4, b5 being Real st b4 < b1 & b1 < b5 holds
ex b6, b7 being Real st
( b4 < b6 & b6 < b1 & b6 in dom (b2 - b3) & b7 < b5 & b1 < b7 & b7 in dom (b2 - b3) ) ) holds
( b2 - b3 is_convergent_in b1 & lim (b2 - b3),b1 = (lim b2,b1) - (lim b3,b1) )
proof end;

theorem Th39: :: LIMFUNC3:39
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b2 " {0} = {} & lim b2,b1 <> 0 holds
( b2 ^ is_convergent_in b1 & lim (b2 ^ ),b1 = (lim b2,b1) " )
proof end;

theorem Th40: :: LIMFUNC3:40
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_convergent_in b1 holds
( abs b2 is_convergent_in b1 & lim (abs b2),b1 = abs (lim b2,b1) )
proof end;

theorem Th41: :: LIMFUNC3:41
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & lim b2,b1 <> 0 & ( for b3, b4 being Real st b3 < b1 & b1 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b1 & b5 in dom b2 & b6 < b4 & b1 < b6 & b6 in dom b2 & b2 . b5 <> 0 & b2 . b6 <> 0 ) ) holds
( b2 ^ is_convergent_in b1 & lim (b2 ^ ),b1 = (lim b2,b1) " )
proof end;

theorem Th42: :: LIMFUNC3:42
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_convergent_in b1 & ( for b4, b5 being Real st b4 < b1 & b1 < b5 holds
ex b6, b7 being Real st
( b4 < b6 & b6 < b1 & b6 in dom (b2 (#) b3) & b7 < b5 & b1 < b7 & b7 in dom (b2 (#) b3) ) ) holds
( b2 (#) b3 is_convergent_in b1 & lim (b2 (#) b3),b1 = (lim b2,b1) * (lim b3,b1) )
proof end;

theorem Th43: :: LIMFUNC3:43
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_convergent_in b1 & lim b3,b1 <> 0 & ( for b4, b5 being Real st b4 < b1 & b1 < b5 holds
ex b6, b7 being Real st
( b4 < b6 & b6 < b1 & b6 in dom (b2 / b3) & b7 < b5 & b1 < b7 & b7 in dom (b2 / b3) ) ) holds
( b2 / b3 is_convergent_in b1 & lim (b2 / b3),b1 = (lim b2,b1) / (lim b3,b1) )
proof end;

theorem Th44: :: LIMFUNC3:44
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & lim b2,b1 = 0 & ( for b4, b5 being Real st b4 < b1 & b1 < b5 holds
ex b6, b7 being Real st
( b4 < b6 & b6 < b1 & b6 in dom (b2 (#) b3) & b7 < b5 & b1 < b7 & b7 in dom (b2 (#) b3) ) ) & ex b4 being Real st
( 0 < b4 & b3 is_bounded_on ].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[ ) holds
( b2 (#) b3 is_convergent_in b1 & lim (b2 (#) b3),b1 = 0 )
proof end;

theorem Th45: :: LIMFUNC3:45
for b1 being Real
for b2, b3, b4 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_convergent_in b1 & lim b2,b1 = lim b3,b1 & ( for b5, b6 being Real st b5 < b1 & b1 < b6 holds
ex b7, b8 being Real st
( b5 < b7 & b7 < b1 & b7 in dom b4 & b8 < b6 & b1 < b8 & b8 in dom b4 ) ) & ex b5 being Real st
( 0 < b5 & ( for b6 being Real st b6 in (dom b4) /\ (].(b1 - b5),b1.[ \/ ].b1,(b1 + b5).[) holds
( b2 . b6 <= b4 . b6 & b4 . b6 <= b3 . b6 ) ) & ( ( (dom b2) /\ (].(b1 - b5),b1.[ \/ ].b1,(b1 + b5).[) c= (dom b3) /\ (].(b1 - b5),b1.[ \/ ].b1,(b1 + b5).[) & (dom b4) /\ (].(b1 - b5),b1.[ \/ ].b1,(b1 + b5).[) c= (dom b2) /\ (].(b1 - b5),b1.[ \/ ].b1,(b1 + b5).[) ) or ( (dom b3) /\ (].(b1 - b5),b1.[ \/ ].b1,(b1 + b5).[) c= (dom b2) /\ (].(b1 - b5),b1.[ \/ ].b1,(b1 + b5).[) & (dom b4) /\ (].(b1 - b5),b1.[ \/ ].b1,(b1 + b5).[) c= (dom b3) /\ (].(b1 - b5),b1.[ \/ ].b1,(b1 + b5).[) ) ) ) holds
( b4 is_convergent_in b1 & lim b4,b1 = lim b2,b1 )
proof end;

theorem Th46: :: LIMFUNC3:46
for b1 being Real
for b2, b3, b4 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_convergent_in b1 & lim b2,b1 = lim b3,b1 & ex b5 being Real st
( 0 < b5 & ].(b1 - b5),b1.[ \/ ].b1,(b1 + b5).[ c= ((dom b2) /\ (dom b3)) /\ (dom b4) & ( for b6 being Real st b6 in ].(b1 - b5),b1.[ \/ ].b1,(b1 + b5).[ holds
( b2 . b6 <= b4 . b6 & b4 . b6 <= b3 . b6 ) ) ) holds
( b4 is_convergent_in b1 & lim b4,b1 = lim b2,b1 )
proof end;

theorem Th47: :: LIMFUNC3:47
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_convergent_in b1 & ex b4 being Real st
( 0 < b4 & ( ( (dom b2) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) c= (dom b3) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) & ( for b5 being Real st b5 in (dom b2) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) holds
b2 . b5 <= b3 . b5 ) ) or ( (dom b3) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) c= (dom b2) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) & ( for b5 being Real st b5 in (dom b3) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) holds
b2 . b5 <= b3 . b5 ) ) ) ) holds
lim b2,b1 <= lim b3,b1
proof end;

theorem Th48: :: LIMFUNC3:48
for b1 being Real
for b2 being PartFunc of REAL , REAL st ( b2 is_divergent_to+infty_in b1 or b2 is_divergent_to-infty_in b1 ) & ( for b3, b4 being Real st b3 < b1 & b1 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b1 & b5 in dom b2 & b6 < b4 & b1 < b6 & b6 in dom b2 & b2 . b5 <> 0 & b2 . b6 <> 0 ) ) holds
( b2 ^ is_convergent_in b1 & lim (b2 ^ ),b1 = 0 )
proof end;

theorem Th49: :: LIMFUNC3:49
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & lim b2,b1 = 0 & ( for b3, b4 being Real st b3 < b1 & b1 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b1 & b5 in dom b2 & b6 < b4 & b1 < b6 & b6 in dom b2 & b2 . b5 <> 0 & b2 . b6 <> 0 ) ) & ex b3 being Real st
( 0 < b3 & ( for b4 being Real st b4 in (dom b2) /\ (].(b1 - b3),b1.[ \/ ].b1,(b1 + b3).[) holds
0 <= b2 . b4 ) ) holds
b2 ^ is_divergent_to+infty_in b1
proof end;

theorem Th50: :: LIMFUNC3:50
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & lim b2,b1 = 0 & ( for b3, b4 being Real st b3 < b1 & b1 < b4 holds
ex b5, b6 being Real st
( b3 < b5 & b5 < b1 & b5 in dom b2 & b6 < b4 & b1 < b6 & b6 in dom b2 & b2 . b5 <> 0 & b2 . b6 <> 0 ) ) & ex b3 being Real st
( 0 < b3 & ( for b4 being Real st b4 in (dom b2) /\ (].(b1 - b3),b1.[ \/ ].b1,(b1 + b3).[) holds
b2 . b4 <= 0 ) ) holds
b2 ^ is_divergent_to-infty_in b1
proof end;

theorem Th51: :: LIMFUNC3:51
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & lim b2,b1 = 0 & ex b3 being Real st
( 0 < b3 & ( for b4 being Real st b4 in (dom b2) /\ (].(b1 - b3),b1.[ \/ ].b1,(b1 + b3).[) holds
0 < b2 . b4 ) ) holds
b2 ^ is_divergent_to+infty_in b1
proof end;

theorem Th52: :: LIMFUNC3:52
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & lim b2,b1 = 0 & ex b3 being Real st
( 0 < b3 & ( for b4 being Real st b4 in (dom b2) /\ (].(b1 - b3),b1.[ \/ ].b1,(b1 + b3).[) holds
b2 . b4 < 0 ) ) holds
b2 ^ is_divergent_to-infty_in b1
proof end;