let f1, f2 be PartFunc of REAL,REAL; :: thesis: for x0 being 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_above ) holds
f1 + f2 is_right_divergent_to-infty_in x0
let x0 be 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_above ) implies f1 + f2 is_right_divergent_to-infty_in x0 )
assume that
A1: f1 is_right_divergent_to-infty_in x0 and
A2: 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_above ) or f1 + f2 is_right_divergent_to-infty_in x0 )
given r being Real such that A3: 0 < r and
A4: f2 | ].x0,(x0 + r).[ is bounded_above ; :: thesis: f1 + f2 is_right_divergent_to-infty_in x0

now :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (f1 + f2)) /\ (right_open_halfline x0) holds
(f1 + f2) /* seq is divergent_to-infty

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 that
A5: seq is convergent and
A6: lim seq = x0 and
A7: rng seq c= (dom (f1 + f2)) /\ (right_open_halfline x0) ; :: thesis: (f1 + f2) /* seq is divergent_to-infty
x0 < x0 + r by A3, Lm2;
then consider k being Nat such that
A8: for n being Nat st k <= n holds
seq . n < x0 + r by A5, A6, LIMFUNC2:2;
A9: (dom (f1 + f2)) /\ (right_open_halfline x0) c= dom (f1 + f2) by XBOOLE_1:17;
A10: rng (seq ^\ k) c= rng seq by VALUED_0:21;
then A11: rng (seq ^\ k) c= (dom (f1 + f2)) /\ (right_open_halfline x0) by A7;
A12: rng (seq ^\ k) c= dom (f1 + f2) by A10, A7, A9;
dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def 1;
then A13: ( dom (f1 + f2) c= dom f1 & dom (f1 + f2) c= dom f2 ) by XBOOLE_1:17;
then A14: ( rng (seq ^\ k) c= dom f1 & rng (seq ^\ k) c= dom f2 ) by A9, A11;
then rng (seq ^\ k) c= (dom f1) /\ (dom f2) by XBOOLE_1:19;
then A15: (f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k)) = (f1 + f2) /* (seq ^\ k) by RFUNCT_2:8
.= ((f1 + f2) /* seq) ^\ k by A7, A9, VALUED_0:27, XBOOLE_1:1 ;
A16: (dom (f1 + f2)) /\ (right_open_halfline x0) c= right_open_halfline x0 by XBOOLE_1:17;
then rng (seq ^\ k) c= right_open_halfline x0 by A10, A7;
then A17: rng (seq ^\ k) c= (dom f1) /\ (right_open_halfline x0) by A14, XBOOLE_1:19;

now :: thesis: ex r2 being set st
for n being Nat holds (f2 /* (seq ^\ k)) . n < r2

consider r1 being Real such that
A18: for g being object st g in ].x0,(x0 + r).[ /\ (dom f2) holds
f2 . g <= r1 by A4, RFUNCT_1:70;
take r2 = r1 + 1; :: thesis: for n being Nat holds (f2 /* (seq ^\ k)) . n < r2
let n be Nat; :: thesis: (f2 /* (seq ^\ k)) . n < r2
A19: n in NAT by ORDINAL1:def 12;
seq . (n + k) < x0 + r by A8, NAT_1:12;
then A20: (seq ^\ k) . n < x0 + r by NAT_1:def 3;
A21: (seq ^\ k) . n in rng (seq ^\ k) by VALUED_0:28;
then (seq ^\ k) . n in right_open_halfline x0 by A10, A7, A16;
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 A20;
then (seq ^\ k) . n in ].x0,(x0 + r).[ by RCOMP_1:def 2;
then (seq ^\ k) . n in ].x0,(x0 + r).[ /\ (dom f2) by A14, A21, XBOOLE_0:def 4;
then f2 . ((seq ^\ k) . n) < r1 + 1 by A18, XREAL_1:39;
hence (f2 /* (seq ^\ k)) . n < r2 by A12, A13, FUNCT_2:108, XBOOLE_1:1, A19; :: thesis: verum

end;

then A22: f2 /* (seq ^\ k) is bounded_above by SEQ_2:def 3;
lim (seq ^\ k) = x0 by A5, A6, SEQ_4:20;
then (f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k)) is divergent_to-infty by A22, A1, A5, A17, LIMFUNC2:def 6, LIMFUNC1:12;
hence (f1 + f2) /* seq is divergent_to-infty by A15, LIMFUNC1:7; :: thesis: verum

end;

hence f1 + f2 is_right_divergent_to-infty_in x0 by A2, LIMFUNC2:def 6; :: thesis: verum