let f1, f2 be PartFunc of REAL,REAL; ( f1 is divergent_in-infty_to-infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 + f2) ) ) & ex r being Real st f2 | (left_open_halfline r) is bounded_above implies f1 + f2 is divergent_in-infty_to-infty )
assume that
A1:
f1 is divergent_in-infty_to-infty
and
A2:
for r being Real ex g being Real st
( g < r & g in dom (f1 + f2) )
; ( for r being Real holds not f2 | (left_open_halfline r) is bounded_above or f1 + f2 is divergent_in-infty_to-infty )
given r1 being Real such that A3:
f2 | (left_open_halfline r1) is bounded_above
; f1 + f2 is divergent_in-infty_to-infty
now for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom (f1 + f2) holds
(f1 + f2) /* seq is divergent_to-infty let seq be
Real_Sequence;
( seq is divergent_to-infty & rng seq c= dom (f1 + f2) implies (f1 + f2) /* seq is divergent_to-infty )assume that A4:
seq is
divergent_to-infty
and A5:
rng seq c= dom (f1 + f2)
;
(f1 + f2) /* seq is divergent_to-infty consider k being
Nat such that A6:
for
n being
Nat st
k <= n holds
seq . n < r1
by A4, LIMFUNC1:def 5;
A7:
rng (seq ^\ k) c= rng seq
by VALUED_0:21;
dom (f1 + f2) = (dom f1) /\ (dom f2)
by A5, Lm1;
then
rng (seq ^\ k) c= (dom f1) /\ (dom f2)
by A5, A7;
then A8:
(f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k)) =
(f1 + f2) /* (seq ^\ k)
by RFUNCT_2:8
.=
((f1 + f2) /* seq) ^\ k
by A5, VALUED_0:27
;
consider r2 being
Real such that A9:
for
g being
object st
g in (left_open_halfline r1) /\ (dom f2) holds
r2 >= f2 . g
by A3, RFUNCT_1:70;
A10:
rng seq c= dom f2
by A5, Lm1;
then A11:
rng (seq ^\ k) c= dom f2
by A7;
then A14:
f2 /* (seq ^\ k) is
bounded_above
by SEQ_2:def 3;
rng seq c= dom f1
by A5, Lm1;
then A15:
rng (seq ^\ k) c= dom f1
by A7;
seq ^\ k is
divergent_to-infty
by A4, LIMFUNC1:27;
then
(f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k)) is
divergent_to-infty
by A1, A14, A15, LIMFUNC1:def 11, LIMFUNC1:12;
hence
(f1 + f2) /* seq is
divergent_to-infty
by A8, LIMFUNC1:7;
verum end;
hence
f1 + f2 is divergent_in-infty_to-infty
by A2, LIMFUNC1:def 11; verum