begin
Lm1:
for g, r being Real st 0 < g holds
( r - g < r & r < r + g )
Lm2:
for f2, f1 being PartFunc of REAL ,REAL
for s being Real_Sequence st rng s c= dom (f2 * f1) holds
( rng s c= dom f1 & rng (f1 /* s) c= dom f2 )
theorem Th1:
theorem Th2:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
for
x0 being
Real for
f1,
f2 being
PartFunc of
REAL ,
REAL st
f1 is_convergent_in x0 &
f2 is_left_convergent_in lim f1,
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 (f2 * f1) &
g2 < r2 &
x0 < g2 &
g2 in dom (f2 * f1) ) ) & ex
g being
Real st
(
0 < g & ( for
r being
Real st
r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r < lim f1,
x0 ) ) holds
(
f2 * f1 is_convergent_in x0 &
lim (f2 * f1),
x0 = lim_left f2,
(lim f1,x0) )
theorem
theorem
for
x0 being
Real for
f1,
f2 being
PartFunc of
REAL ,
REAL st
f1 is_convergent_in x0 &
f2 is_right_convergent_in lim f1,
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 (f2 * f1) &
g2 < r2 &
x0 < g2 &
g2 in dom (f2 * f1) ) ) & ex
g being
Real st
(
0 < g & ( for
r being
Real st
r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
lim f1,
x0 < f1 . r ) ) holds
(
f2 * f1 is_convergent_in x0 &
lim (f2 * f1),
x0 = lim_right f2,
(lim f1,x0) )
theorem
theorem
for
x0 being
Real for
f1,
f2 being
PartFunc of
REAL ,
REAL st
f1 is_convergent_in x0 &
f2 is_convergent_in lim f1,
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 (f2 * f1) &
g2 < r2 &
x0 < g2 &
g2 in dom (f2 * f1) ) ) & ex
g being
Real st
(
0 < g & ( for
r being
Real st
r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r <> lim f1,
x0 ) ) holds
(
f2 * f1 is_convergent_in x0 &
lim (f2 * f1),
x0 = lim f2,
(lim f1,x0) )