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
( r < g & g in dom (f1 + f2) ) ) & ex r being Real st f2 | (right_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
( r < g & g in dom (f1 + f2) ) ; :: thesis: ( for r being Real holds not f2 | (right_open_halfline r) is bounded_above or f1 + f2 is divergent_in+infty_to-infty )
given r1 being Real such that A3: f2 | (right_open_halfline r1) is bounded_above ; :: thesis: f1 + f2 is divergent_in+infty_to-infty

now :: thesis: 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; :: thesis: ( 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) ; :: thesis: (f1 + f2) /* seq is divergent_to-infty
consider k being Nat such that
A6: for n being Nat st k <= n holds
r1 < seq . n by A4, LIMFUNC1:def 4;
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 (right_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;

now :: thesis: for n being Nat holds |.r2.| + 1 > (f2 /* (seq ^\ k)) . n

let n be Nat; :: thesis: |.r2.| + 1 > (f2 /* (seq ^\ k)) . n
A12: n in NAT by ORDINAL1:def 12;
reconsider nk = n + k, nn = n as Element of NAT by ORDINAL1:def 12;
r1 < seq . nk by A6, NAT_1:12;
then ( (seq ^\ k) . nn < +infty & r1 < (seq ^\ k) . nn ) by NAT_1:def 3, XXREAL_0:9;
then ( (seq ^\ k) . n in rng (seq ^\ k) & (seq ^\ k) . n in right_open_halfline r1 ) by VALUED_0:28, XXREAL_1:4;
then (seq ^\ k) . n in (right_open_halfline r1) /\ (dom f2) by A11, XBOOLE_0:def 4;
then r2 >= f2 . ((seq ^\ k) . n) by A9;
then A13: r2 >= (f2 /* (seq ^\ k)) . n by A10, A7, FUNCT_2:108, XBOOLE_1:1, A12;
( r2 <= |.r2.| & |.r2.| < |.r2.| + 1 ) by ABSVALUE:4, XREAL_1:29;
then r2 < |.r2.| + 1 by XXREAL_0:2;
hence |.r2.| + 1 > (f2 /* (seq ^\ k)) . n by A13, XXREAL_0:2; :: thesis: verum

end;

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:26;
then (f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k)) is divergent_to-infty by A1, A14, A15, LIMFUNC1:def 8, LIMFUNC1:12;
hence (f1 + f2) /* seq is divergent_to-infty by A8, LIMFUNC1:7; :: thesis: verum

end;

hence f1 + f2 is divergent_in+infty_to-infty by A2, LIMFUNC1:def 8; :: thesis: verum