let x0 be Real; :: thesis: 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
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( 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 ) implies f1 + f2 is_right_divergent_to+infty_in x0 )
assume A1:
( 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) ) ) )
; :: thesis: ( for r being Real holds
( not 0 < r or not f2 | ].x0,(x0 + r).[ is bounded_below ) or f1 + f2 is_right_divergent_to+infty_in x0 )
given r being Real such that A2:
( 0 < r & f2 | ].x0,(x0 + r).[ is bounded_below )
; :: thesis: f1 + f2 is_right_divergent_to+infty_in x0
now let seq be
Real_Sequence;
:: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (f1 + f2)) /\ (right_open_halfline x0) implies (f1 + f2) /* seq is divergent_to+infty )assume A3:
(
seq is
convergent &
lim seq = x0 &
rng seq c= (dom (f1 + f2)) /\ (right_open_halfline x0) )
;
:: thesis: (f1 + f2) /* seq is divergent_to+infty
x0 < x0 + r
by A2, Lm1;
then consider k being
Element of
NAT such that A4:
for
n being
Element of
NAT st
k <= n holds
seq . n < x0 + r
by A3, Th2;
A5:
(
seq ^\ k is
convergent &
lim (seq ^\ k) = x0 )
by A3, SEQ_4:33;
rng (seq ^\ k) c= rng seq
by VALUED_0:21;
then A6:
rng (seq ^\ k) c= (dom (f1 + f2)) /\ (right_open_halfline x0)
by A3, XBOOLE_1:1;
A7:
(
(dom (f1 + f2)) /\ (right_open_halfline x0) c= dom (f1 + f2) &
(dom (f1 + f2)) /\ (right_open_halfline x0) c= right_open_halfline x0 )
by XBOOLE_1:17;
then A8:
(
rng (seq ^\ k) c= dom (f1 + f2) &
rng (seq ^\ k) c= right_open_halfline x0 )
by A6, XBOOLE_1:1;
dom (f1 + f2) = (dom f1) /\ (dom f2)
by VALUED_1:def 1;
then A9:
(
dom (f1 + f2) c= dom f1 &
dom (f1 + f2) c= dom f2 )
by XBOOLE_1:17;
then A10:
(
rng (seq ^\ k) c= dom f1 &
rng (seq ^\ k) c= dom f2 )
by A8, XBOOLE_1:1;
then
rng (seq ^\ k) c= (dom f1) /\ (right_open_halfline x0)
by A8, XBOOLE_1:19;
then A11:
f1 /* (seq ^\ k) is
divergent_to+infty
by A1, A5, Def5;
A12:
rng (seq ^\ k) c= (dom f1) /\ (dom f2)
by A10, XBOOLE_1:19;
now consider r1 being
real number such that A13:
for
g being
set st
g in ].x0,(x0 + r).[ /\ (dom f2) holds
r1 <= f2 . g
by A2, RFUNCT_1:88;
take r2 =
r1 - 1;
:: thesis: for n being Element of NAT holds r2 < (f2 /* (seq ^\ k)) . nlet n be
Element of
NAT ;
:: thesis: r2 < (f2 /* (seq ^\ k)) . n
seq . (n + k) < x0 + r
by A4, NAT_1:12;
then A14:
(seq ^\ k) . n < x0 + r
by NAT_1:def 3;
A15:
(seq ^\ k) . n in rng (seq ^\ k)
by VALUED_0:28;
then
(seq ^\ k) . n in right_open_halfline x0
by A8;
then
(seq ^\ k) . n in { g1 where g1 is Real : x0 < g1 }
by XXREAL_1:230;
then
ex
g being
Real st
(
g = (seq ^\ k) . n &
x0 < g )
;
then
(seq ^\ k) . n in { g2 where g2 is Real : ( x0 < g2 & g2 < x0 + r ) }
by A14;
then
(seq ^\ k) . n in ].x0,(x0 + r).[
by RCOMP_1:def 2;
then
(seq ^\ k) . n in ].x0,(x0 + r).[ /\ (dom f2)
by A10, A15, XBOOLE_0:def 4;
then
r1 <= f2 . ((seq ^\ k) . n)
by A13;
then
r1 - 1
< (f2 . ((seq ^\ k) . n)) - 0
by XREAL_1:17;
hence
r2 < (f2 /* (seq ^\ k)) . n
by A8, A9, FUNCT_2:185, XBOOLE_1:1;
:: thesis: verum end; then
f2 /* (seq ^\ k) is
bounded_below
by SEQ_2:def 4;
then A16:
(f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k)) is
divergent_to+infty
by A11, LIMFUNC1:36;
(f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k)) =
(f1 + f2) /* (seq ^\ k)
by A12, RFUNCT_2:23
.=
((f1 + f2) /* seq) ^\ k
by A3, A7, VALUED_0:27, XBOOLE_1:1
;
hence
(f1 + f2) /* seq is
divergent_to+infty
by A16, LIMFUNC1:34;
:: thesis: verum end;
hence
f1 + f2 is_right_divergent_to+infty_in x0
by A1, Def5; :: thesis: verum