let f1, f2 be PartFunc of REAL , REAL ; :: thesis: ( 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_below implies f1 + f2 is divergent_in-infty_to+infty )
assume A1: ( f1 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 + f2) ) ) ) ; :: thesis: ( for r being Real holds not f2 | (left_open_halfline r) is bounded_below or f1 + f2 is divergent_in-infty_to+infty )
given r1 being Real such that A2: f2 | (left_open_halfline r1) is bounded_below ; :: thesis: f1 + f2 is divergent_in-infty_to+infty

now

let seq be Real_Sequence; :: thesis: ( seq is divergent_to-infty & rng seq c= dom (f1 + f2) implies (f1 + f2) /* seq is divergent_to+infty )
assume A3: ( seq is divergent_to-infty & rng seq c= dom (f1 + f2) ) ; :: thesis: (f1 + f2) /* seq is divergent_to+infty
then A4: ( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 ) by Lm2;
consider k being Element of NAT such that
A5: for n being Element of NAT st k <= n holds
seq . n < r1 by A3, Def5;
A6: seq ^\ k is divergent_to-infty by A3, Th54;
A7: rng (seq ^\ k) c= rng seq by VALUED_0:21;
then A8: ( rng (seq ^\ k) c= dom f1 & rng (seq ^\ k) c= dom f2 ) by A4, XBOOLE_1:1;
then A9: f1 /* (seq ^\ k) is divergent_to+infty by A1, A6, Def10;
consider r2 being real number such that
A10: for g being set st g in (left_open_halfline r1) /\ (dom f2) holds
r2 <= f2 . g by A2, RFUNCT_1:88;

now

let n be Element of NAT ; :: thesis: (- (abs r2)) - 1 < (f2 /* (seq ^\ k)) . n
A11: (seq ^\ k) . n in rng (seq ^\ k) by VALUED_0:28;
seq . (n + k) < r1 by A5, NAT_1:12;
then (seq ^\ k) . n < r1 by NAT_1:def 3;
then (seq ^\ k) . n in { g2 where g2 is Real : g2 < r1 } ;
then (seq ^\ k) . n in left_open_halfline r1 by XXREAL_1:229;
then (seq ^\ k) . n in (left_open_halfline r1) /\ (dom f2) by A8, A11, XBOOLE_0:def 4;
then r2 <= f2 . ((seq ^\ k) . n) by A10;
then A12: r2 <= (f2 /* (seq ^\ k)) . n by A4, A7, FUNCT_2:185, XBOOLE_1:1;
- (abs r2) <= r2 by ABSVALUE:11;
then (- (abs r2)) - 1 < r2 - 0 by XREAL_1:17;
hence (- (abs r2)) - 1 < (f2 /* (seq ^\ k)) . n by A12, XXREAL_0:2; :: thesis: verum

end;

then f2 /* (seq ^\ k) is bounded_below by SEQ_2:def 4;
then A13: (f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k)) is divergent_to+infty by A9, Th36;
rng (seq ^\ k) c= (dom f1) /\ (dom f2) by A3, A4, A7, XBOOLE_1:1;
then (f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k)) = (f1 + f2) /* (seq ^\ k) by RFUNCT_2:23
.= ((f1 + f2) /* seq) ^\ k by A3, VALUED_0:27 ;
hence (f1 + f2) /* seq is divergent_to+infty by A13, Th34; :: thesis: verum

end;

hence f1 + f2 is divergent_in-infty_to+infty by A1, Def10; :: thesis: verum