:: LIMFUNC4 semantic presentation

Lemma1: for b1, b2 being Real st 0 < b1 holds
( b2 - b1 < b2 & b2 < b2 + b1 )
proof end;

Lemma2: for b1, b2 being PartFunc of REAL , REAL
for b3 being Real_Sequence st rng b3 c= dom (b1 * b2) holds
( rng b3 c= dom b2 & rng (b2 * b3) c= dom b1 )
proof end;

theorem Th1: :: LIMFUNC4:1
for b1, b2 being PartFunc of REAL , REAL
for b3 being Real_Sequence
for b4 being set st rng b3 c= (dom (b1 * b2)) /\ b4 holds
( rng b3 c= dom (b1 * b2) & rng b3 c= b4 & rng b3 c= dom b2 & rng b3 c= (dom b2) /\ b4 & rng (b2 * b3) c= dom b1 )
proof end;

theorem Th2: :: LIMFUNC4:2
for b1, b2 being PartFunc of REAL , REAL
for b3 being Real_Sequence
for b4 being set st rng b3 c= (dom (b1 * b2)) \ b4 holds
( rng b3 c= dom (b1 * b2) & rng b3 c= dom b2 & rng b3 c= (dom b2) \ b4 & rng (b2 * b3) c= dom b1 )
proof end;

theorem Th3: :: LIMFUNC4:3
for b1, b2 being PartFunc of REAL , REAL st b1 is divergent_in+infty_to+infty & b2 is divergent_in+infty_to+infty & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) holds
b2 * b1 is divergent_in+infty_to+infty
proof end;

theorem Th4: :: LIMFUNC4:4
for b1, b2 being PartFunc of REAL , REAL st b1 is divergent_in+infty_to+infty & b2 is divergent_in+infty_to-infty & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) holds
b2 * b1 is divergent_in+infty_to-infty
proof end;

theorem Th5: :: LIMFUNC4:5
for b1, b2 being PartFunc of REAL , REAL st b1 is divergent_in+infty_to-infty & b2 is divergent_in-infty_to+infty & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) holds
b2 * b1 is divergent_in+infty_to+infty
proof end;

theorem Th6: :: LIMFUNC4:6
for b1, b2 being PartFunc of REAL , REAL st b1 is divergent_in+infty_to-infty & b2 is divergent_in-infty_to-infty & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) holds
b2 * b1 is divergent_in+infty_to-infty
proof end;

theorem Th7: :: LIMFUNC4:7
for b1, b2 being PartFunc of REAL , REAL st b1 is divergent_in-infty_to+infty & b2 is divergent_in+infty_to+infty & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) holds
b2 * b1 is divergent_in-infty_to+infty
proof end;

theorem Th8: :: LIMFUNC4:8
for b1, b2 being PartFunc of REAL , REAL st b1 is divergent_in-infty_to+infty & b2 is divergent_in+infty_to-infty & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) holds
b2 * b1 is divergent_in-infty_to-infty
proof end;

theorem Th9: :: LIMFUNC4:9
for b1, b2 being PartFunc of REAL , REAL st b1 is divergent_in-infty_to-infty & b2 is divergent_in-infty_to+infty & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) holds
b2 * b1 is divergent_in-infty_to+infty
proof end;

theorem Th10: :: LIMFUNC4:10
for b1, b2 being PartFunc of REAL , REAL st b1 is divergent_in-infty_to-infty & b2 is divergent_in-infty_to-infty & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) holds
b2 * b1 is divergent_in-infty_to-infty
proof end;

theorem Th11: :: LIMFUNC4:11
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_divergent_to+infty_in b1 & b3 is divergent_in+infty_to+infty & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) holds
b3 * b2 is_left_divergent_to+infty_in b1
proof end;

theorem Th12: :: LIMFUNC4:12
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_divergent_to+infty_in b1 & b3 is divergent_in+infty_to-infty & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) holds
b3 * b2 is_left_divergent_to-infty_in b1
proof end;

theorem Th13: :: LIMFUNC4:13
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_divergent_to-infty_in b1 & b3 is divergent_in-infty_to+infty & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) holds
b3 * b2 is_left_divergent_to+infty_in b1
proof end;

theorem Th14: :: LIMFUNC4:14
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_divergent_to-infty_in b1 & b3 is divergent_in-infty_to-infty & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) holds
b3 * b2 is_left_divergent_to-infty_in b1
proof end;

theorem Th15: :: LIMFUNC4:15
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_divergent_to+infty_in b1 & b3 is divergent_in+infty_to+infty & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) holds
b3 * b2 is_right_divergent_to+infty_in b1
proof end;

theorem Th16: :: LIMFUNC4:16
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_divergent_to+infty_in b1 & b3 is divergent_in+infty_to-infty & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) holds
b3 * b2 is_right_divergent_to-infty_in b1
proof end;

theorem Th17: :: LIMFUNC4:17
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_divergent_to-infty_in b1 & b3 is divergent_in-infty_to+infty & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) holds
b3 * b2 is_right_divergent_to+infty_in b1
proof end;

theorem Th18: :: LIMFUNC4:18
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_divergent_to-infty_in b1 & b3 is divergent_in-infty_to-infty & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) holds
b3 * b2 is_right_divergent_to-infty_in b1
proof end;

theorem Th19: :: LIMFUNC4:19
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_convergent_in b1 & b3 is_left_divergent_to+infty_in lim_left b2,b1 & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].(b1 - b4),b1.[ holds
b2 . b5 < lim_left b2,b1 ) ) holds
b3 * b2 is_left_divergent_to+infty_in b1
proof end;

theorem Th20: :: LIMFUNC4:20
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_convergent_in b1 & b3 is_left_divergent_to-infty_in lim_left b2,b1 & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].(b1 - b4),b1.[ holds
b2 . b5 < lim_left b2,b1 ) ) holds
b3 * b2 is_left_divergent_to-infty_in b1
proof end;

theorem Th21: :: LIMFUNC4:21
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_convergent_in b1 & b3 is_right_divergent_to+infty_in lim_left b2,b1 & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].(b1 - b4),b1.[ holds
lim_left b2,b1 < b2 . b5 ) ) holds
b3 * b2 is_left_divergent_to+infty_in b1
proof end;

theorem Th22: :: LIMFUNC4:22
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_convergent_in b1 & b3 is_right_divergent_to-infty_in lim_left b2,b1 & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].(b1 - b4),b1.[ holds
lim_left b2,b1 < b2 . b5 ) ) holds
b3 * b2 is_left_divergent_to-infty_in b1
proof end;

theorem Th23: :: LIMFUNC4:23
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_convergent_in b1 & b3 is_right_divergent_to+infty_in lim_right b2,b1 & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].b1,(b1 + b4).[ holds
lim_right b2,b1 < b2 . b5 ) ) holds
b3 * b2 is_right_divergent_to+infty_in b1
proof end;

theorem Th24: :: LIMFUNC4:24
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_convergent_in b1 & b3 is_right_divergent_to-infty_in lim_right b2,b1 & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].b1,(b1 + b4).[ holds
lim_right b2,b1 < b2 . b5 ) ) holds
b3 * b2 is_right_divergent_to-infty_in b1
proof end;

theorem Th25: :: LIMFUNC4:25
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_convergent_in b1 & b3 is_left_divergent_to+infty_in lim_right b2,b1 & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].b1,(b1 + b4).[ holds
b2 . b5 < lim_right b2,b1 ) ) holds
b3 * b2 is_right_divergent_to+infty_in b1
proof end;

theorem Th26: :: LIMFUNC4:26
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_convergent_in b1 & b3 is_left_divergent_to-infty_in lim_right b2,b1 & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].b1,(b1 + b4).[ holds
b2 . b5 < lim_right b2,b1 ) ) holds
b3 * b2 is_right_divergent_to-infty_in b1
proof end;

theorem Th27: :: LIMFUNC4:27
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in+infty & b2 is_left_divergent_to+infty_in lim_in+infty b1 & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (right_open_halfline b3) holds
b1 . b4 < lim_in+infty b1 holds
b2 * b1 is divergent_in+infty_to+infty
proof end;

theorem Th28: :: LIMFUNC4:28
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in+infty & b2 is_left_divergent_to-infty_in lim_in+infty b1 & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (right_open_halfline b3) holds
b1 . b4 < lim_in+infty b1 holds
b2 * b1 is divergent_in+infty_to-infty
proof end;

theorem Th29: :: LIMFUNC4:29
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in+infty & b2 is_right_divergent_to+infty_in lim_in+infty b1 & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (right_open_halfline b3) holds
lim_in+infty b1 < b1 . b4 holds
b2 * b1 is divergent_in+infty_to+infty
proof end;

theorem Th30: :: LIMFUNC4:30
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in+infty & b2 is_right_divergent_to-infty_in lim_in+infty b1 & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (right_open_halfline b3) holds
lim_in+infty b1 < b1 . b4 holds
b2 * b1 is divergent_in+infty_to-infty
proof end;

theorem Th31: :: LIMFUNC4:31
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in-infty & b2 is_left_divergent_to+infty_in lim_in-infty b1 & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (left_open_halfline b3) holds
b1 . b4 < lim_in-infty b1 holds
b2 * b1 is divergent_in-infty_to+infty
proof end;

theorem Th32: :: LIMFUNC4:32
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in-infty & b2 is_left_divergent_to-infty_in lim_in-infty b1 & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (left_open_halfline b3) holds
b1 . b4 < lim_in-infty b1 holds
b2 * b1 is divergent_in-infty_to-infty
proof end;

theorem Th33: :: LIMFUNC4:33
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in-infty & b2 is_right_divergent_to+infty_in lim_in-infty b1 & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (left_open_halfline b3) holds
lim_in-infty b1 < b1 . b4 holds
b2 * b1 is divergent_in-infty_to+infty
proof end;

theorem Th34: :: LIMFUNC4:34
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in-infty & b2 is_right_divergent_to-infty_in lim_in-infty b1 & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (left_open_halfline b3) holds
lim_in-infty b1 < b1 . b4 holds
b2 * b1 is divergent_in-infty_to-infty
proof end;

theorem Th35: :: LIMFUNC4:35
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_divergent_to+infty_in b1 & b3 is divergent_in+infty_to+infty & ( 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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) holds
b3 * b2 is_divergent_to+infty_in b1
proof end;

theorem Th36: :: LIMFUNC4:36
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_divergent_to+infty_in b1 & b3 is divergent_in+infty_to-infty & ( 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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) holds
b3 * b2 is_divergent_to-infty_in b1
proof end;

theorem Th37: :: LIMFUNC4:37
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_divergent_to-infty_in b1 & b3 is divergent_in-infty_to+infty & ( 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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) holds
b3 * b2 is_divergent_to+infty_in b1
proof end;

theorem Th38: :: LIMFUNC4:38
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_divergent_to-infty_in b1 & b3 is divergent_in-infty_to-infty & ( 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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) holds
b3 * b2 is_divergent_to-infty_in b1
proof end;

theorem Th39: :: LIMFUNC4:39
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_divergent_to+infty_in lim b2,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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) holds
b2 . b5 <> lim b2,b1 ) ) holds
b3 * b2 is_divergent_to+infty_in b1
proof end;

theorem Th40: :: LIMFUNC4:40
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_divergent_to-infty_in lim b2,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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) holds
b2 . b5 <> lim b2,b1 ) ) holds
b3 * b2 is_divergent_to-infty_in b1
proof end;

theorem Th41: :: LIMFUNC4:41
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_right_divergent_to+infty_in lim b2,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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) holds
b2 . b5 > lim b2,b1 ) ) holds
b3 * b2 is_divergent_to+infty_in b1
proof end;

theorem Th42: :: LIMFUNC4:42
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_right_divergent_to-infty_in lim b2,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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) holds
b2 . b5 > lim b2,b1 ) ) holds
b3 * b2 is_divergent_to-infty_in b1
proof end;

theorem Th43: :: LIMFUNC4:43
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_convergent_in b1 & b3 is_divergent_to+infty_in lim_right b2,b1 & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].b1,(b1 + b4).[ holds
b2 . b5 <> lim_right b2,b1 ) ) holds
b3 * b2 is_right_divergent_to+infty_in b1
proof end;

theorem Th44: :: LIMFUNC4:44
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_convergent_in b1 & b3 is_divergent_to-infty_in lim_right b2,b1 & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].b1,(b1 + b4).[ holds
b2 . b5 <> lim_right b2,b1 ) ) holds
b3 * b2 is_right_divergent_to-infty_in b1
proof end;

theorem Th45: :: LIMFUNC4:45
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in+infty & b2 is_divergent_to+infty_in lim_in+infty b1 & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (right_open_halfline b3) holds
b1 . b4 <> lim_in+infty b1 holds
b2 * b1 is divergent_in+infty_to+infty
proof end;

theorem Th46: :: LIMFUNC4:46
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in+infty & b2 is_divergent_to-infty_in lim_in+infty b1 & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (right_open_halfline b3) holds
b1 . b4 <> lim_in+infty b1 holds
b2 * b1 is divergent_in+infty_to-infty
proof end;

theorem Th47: :: LIMFUNC4:47
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in-infty & b2 is_divergent_to+infty_in lim_in-infty b1 & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (left_open_halfline b3) holds
b1 . b4 <> lim_in-infty b1 holds
b2 * b1 is divergent_in-infty_to+infty
proof end;

theorem Th48: :: LIMFUNC4:48
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in-infty & b2 is_divergent_to-infty_in lim_in-infty b1 & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (left_open_halfline b3) holds
b1 . b4 <> lim_in-infty b1 holds
b2 * b1 is divergent_in-infty_to-infty
proof end;

theorem Th49: :: LIMFUNC4:49
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_left_divergent_to+infty_in lim b2,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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) holds
b2 . b5 < lim b2,b1 ) ) holds
b3 * b2 is_divergent_to+infty_in b1
proof end;

theorem Th50: :: LIMFUNC4:50
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_left_divergent_to-infty_in lim b2,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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) holds
b2 . b5 < lim b2,b1 ) ) holds
b3 * b2 is_divergent_to-infty_in b1
proof end;

theorem Th51: :: LIMFUNC4:51
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_convergent_in b1 & b3 is_divergent_to+infty_in lim_left b2,b1 & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].(b1 - b4),b1.[ holds
b2 . b5 <> lim_left b2,b1 ) ) holds
b3 * b2 is_left_divergent_to+infty_in b1
proof end;

theorem Th52: :: LIMFUNC4:52
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_convergent_in b1 & b3 is_divergent_to-infty_in lim_left b2,b1 & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].(b1 - b4),b1.[ holds
b2 . b5 <> lim_left b2,b1 ) ) holds
b3 * b2 is_left_divergent_to-infty_in b1
proof end;

theorem Th53: :: LIMFUNC4:53
for b1, b2 being PartFunc of REAL , REAL st b1 is divergent_in+infty_to+infty & b2 is convergent_in+infty & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) holds
( b2 * b1 is convergent_in+infty & lim_in+infty (b2 * b1) = lim_in+infty b2 )
proof end;

theorem Th54: :: LIMFUNC4:54
for b1, b2 being PartFunc of REAL , REAL st b1 is divergent_in+infty_to-infty & b2 is convergent_in-infty & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) holds
( b2 * b1 is convergent_in+infty & lim_in+infty (b2 * b1) = lim_in-infty b2 )
proof end;

theorem Th55: :: LIMFUNC4:55
for b1, b2 being PartFunc of REAL , REAL st b1 is divergent_in-infty_to+infty & b2 is convergent_in+infty & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) holds
( b2 * b1 is convergent_in-infty & lim_in-infty (b2 * b1) = lim_in+infty b2 )
proof end;

theorem Th56: :: LIMFUNC4:56
for b1, b2 being PartFunc of REAL , REAL st b1 is divergent_in-infty_to-infty & b2 is convergent_in-infty & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) holds
( b2 * b1 is convergent_in-infty & lim_in-infty (b2 * b1) = lim_in-infty b2 )
proof end;

theorem Th57: :: LIMFUNC4:57
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_divergent_to+infty_in b1 & b3 is convergent_in+infty & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) holds
( b3 * b2 is_left_convergent_in b1 & lim_left (b3 * b2),b1 = lim_in+infty b3 )
proof end;

theorem Th58: :: LIMFUNC4:58
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_divergent_to-infty_in b1 & b3 is convergent_in-infty & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) holds
( b3 * b2 is_left_convergent_in b1 & lim_left (b3 * b2),b1 = lim_in-infty b3 )
proof end;

theorem Th59: :: LIMFUNC4:59
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_divergent_to+infty_in b1 & b3 is convergent_in+infty & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) holds
( b3 * b2 is_right_convergent_in b1 & lim_right (b3 * b2),b1 = lim_in+infty b3 )
proof end;

theorem Th60: :: LIMFUNC4:60
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_divergent_to-infty_in b1 & b3 is convergent_in-infty & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) holds
( b3 * b2 is_right_convergent_in b1 & lim_right (b3 * b2),b1 = lim_in-infty b3 )
proof end;

theorem Th61: :: LIMFUNC4:61
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_convergent_in b1 & b3 is_left_convergent_in lim_left b2,b1 & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].(b1 - b4),b1.[ holds
b2 . b5 < lim_left b2,b1 ) ) holds
( b3 * b2 is_left_convergent_in b1 & lim_left (b3 * b2),b1 = lim_left b3,(lim_left b2,b1) )
proof end;

theorem Th62: :: LIMFUNC4:62
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_convergent_in b1 & b3 is_right_convergent_in lim_right b2,b1 & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].b1,(b1 + b4).[ holds
lim_right b2,b1 < b2 . b5 ) ) holds
( b3 * b2 is_right_convergent_in b1 & lim_right (b3 * b2),b1 = lim_right b3,(lim_right b2,b1) )
proof end;

theorem Th63: :: LIMFUNC4:63
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_convergent_in b1 & b3 is_right_convergent_in lim_left b2,b1 & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].(b1 - b4),b1.[ holds
lim_left b2,b1 < b2 . b5 ) ) holds
( b3 * b2 is_left_convergent_in b1 & lim_left (b3 * b2),b1 = lim_right b3,(lim_left b2,b1) )
proof end;

theorem Th64: :: LIMFUNC4:64
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_convergent_in b1 & b3 is_left_convergent_in lim_right b2,b1 & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].b1,(b1 + b4).[ holds
b2 . b5 < lim_right b2,b1 ) ) holds
( b3 * b2 is_right_convergent_in b1 & lim_right (b3 * b2),b1 = lim_left b3,(lim_right b2,b1) )
proof end;

theorem Th65: :: LIMFUNC4:65
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in+infty & b2 is_left_convergent_in lim_in+infty b1 & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (right_open_halfline b3) holds
b1 . b4 < lim_in+infty b1 holds
( b2 * b1 is convergent_in+infty & lim_in+infty (b2 * b1) = lim_left b2,(lim_in+infty b1) )
proof end;

theorem Th66: :: LIMFUNC4:66
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in+infty & b2 is_right_convergent_in lim_in+infty b1 & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (right_open_halfline b3) holds
lim_in+infty b1 < b1 . b4 holds
( b2 * b1 is convergent_in+infty & lim_in+infty (b2 * b1) = lim_right b2,(lim_in+infty b1) )
proof end;

theorem Th67: :: LIMFUNC4:67
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in-infty & b2 is_left_convergent_in lim_in-infty b1 & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (left_open_halfline b3) holds
b1 . b4 < lim_in-infty b1 holds
( b2 * b1 is convergent_in-infty & lim_in-infty (b2 * b1) = lim_left b2,(lim_in-infty b1) )
proof end;

theorem Th68: :: LIMFUNC4:68
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in-infty & b2 is_right_convergent_in lim_in-infty b1 & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (left_open_halfline b3) holds
lim_in-infty b1 < b1 . b4 holds
( b2 * b1 is convergent_in-infty & lim_in-infty (b2 * b1) = lim_right b2,(lim_in-infty b1) )
proof end;

theorem Th69: :: LIMFUNC4:69
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_divergent_to+infty_in b1 & b3 is convergent_in+infty & ( 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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) holds
( b3 * b2 is_convergent_in b1 & lim (b3 * b2),b1 = lim_in+infty b3 )
proof end;

theorem Th70: :: LIMFUNC4:70
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_divergent_to-infty_in b1 & b3 is convergent_in-infty & ( 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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) holds
( b3 * b2 is_convergent_in b1 & lim (b3 * b2),b1 = lim_in-infty b3 )
proof end;

theorem Th71: :: LIMFUNC4:71
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in+infty & b2 is_convergent_in lim_in+infty b1 & ( for b3 being Real ex b4 being Real st
( b3 < b4 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (right_open_halfline b3) holds
b1 . b4 <> lim_in+infty b1 holds
( b2 * b1 is convergent_in+infty & lim_in+infty (b2 * b1) = lim b2,(lim_in+infty b1) )
proof end;

theorem Th72: :: LIMFUNC4:72
for b1, b2 being PartFunc of REAL , REAL st b1 is convergent_in-infty & b2 is_convergent_in lim_in-infty b1 & ( for b3 being Real ex b4 being Real st
( b4 < b3 & b4 in dom (b2 * b1) ) ) & ex b3 being Real st
for b4 being Real st b4 in (dom b1) /\ (left_open_halfline b3) holds
b1 . b4 <> lim_in-infty b1 holds
( b2 * b1 is convergent_in-infty & lim_in-infty (b2 * b1) = lim b2,(lim_in-infty b1) )
proof end;

theorem Th73: :: LIMFUNC4:73
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_left_convergent_in lim b2,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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) holds
b2 . b5 < lim b2,b1 ) ) holds
( b3 * b2 is_convergent_in b1 & lim (b3 * b2),b1 = lim_left b3,(lim b2,b1) )
proof end;

theorem Th74: :: LIMFUNC4:74
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_left_convergent_in b1 & b3 is_convergent_in lim_left b2,b1 & ( for b4 being Real st b4 < b1 holds
ex b5 being Real st
( b4 < b5 & b5 < b1 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].(b1 - b4),b1.[ holds
b2 . b5 <> lim_left b2,b1 ) ) holds
( b3 * b2 is_left_convergent_in b1 & lim_left (b3 * b2),b1 = lim b3,(lim_left b2,b1) )
proof end;

theorem Th75: :: LIMFUNC4:75
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_right_convergent_in lim b2,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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) holds
lim b2,b1 < b2 . b5 ) ) holds
( b3 * b2 is_convergent_in b1 & lim (b3 * b2),b1 = lim_right b3,(lim b2,b1) )
proof end;

theorem Th76: :: LIMFUNC4:76
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_right_convergent_in b1 & b3 is_convergent_in lim_right b2,b1 & ( for b4 being Real st b1 < b4 holds
ex b5 being Real st
( b5 < b4 & b1 < b5 & b5 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ ].b1,(b1 + b4).[ holds
b2 . b5 <> lim_right b2,b1 ) ) holds
( b3 * b2 is_right_convergent_in b1 & lim_right (b3 * b2),b1 = lim b3,(lim_right b2,b1) )
proof end;

theorem Th77: :: LIMFUNC4:77
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_convergent_in b1 & b3 is_convergent_in lim b2,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 * b2) & b7 < b5 & b1 < b7 & b7 in dom (b3 * b2) ) ) & ex b4 being Real st
( 0 < b4 & ( for b5 being Real st b5 in (dom b2) /\ (].(b1 - b4),b1.[ \/ ].b1,(b1 + b4).[) holds
b2 . b5 <> lim b2,b1 ) ) holds
( b3 * b2 is_convergent_in b1 & lim (b3 * b2),b1 = lim b3,(lim b2,b1) )
proof end;