let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st f1 is_divergent_to+infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 + f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 + f2) ) ) & ex r being Real st
( 0 < r & f2 | (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) is bounded_below ) holds
f1 + f2 is_divergent_to+infty_in x0
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_divergent_to+infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 + f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 + f2) ) ) & ex r being Real st
( 0 < r & f2 | (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) is bounded_below ) implies f1 + f2 is_divergent_to+infty_in x0 )
assume A1: ( f1 is_divergent_to+infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 + f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 + f2) ) ) ) ; :: thesis: ( for r being Real holds
( not 0 < r or not f2 | (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) is bounded_below ) or f1 + f2 is_divergent_to+infty_in x0 )
given r being Real such that A2: ( 0 < r & f2 | (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) is bounded_below ) ; :: thesis: f1 + f2 is_divergent_to+infty_in x0

now

let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom (f1 + f2)) \ {x0} implies (f1 + f2) /* s is divergent_to+infty )
assume A3: ( s is convergent & lim s = x0 & rng s c= (dom (f1 + f2)) \ {x0} ) ; :: thesis: (f1 + f2) /* s is divergent_to+infty
then consider k being Element of NAT such that
A4: for n being Element of NAT st k <= n holds
( x0 - r < s . n & s . n < x0 + r ) by A2, Th7;
A5: ( s ^\ k is convergent & lim (s ^\ k) = x0 ) by A3, SEQ_4:33;
rng (s ^\ k) c= rng s by VALUED_0:21;
then A6: rng (s ^\ k) c= (dom (f1 + f2)) \ {x0} by A3, XBOOLE_1:1;
then A7: ( rng (s ^\ k) c= dom (f1 + f2) & rng (s ^\ k) c= dom f1 & rng (s ^\ k) c= dom f2 & rng (s ^\ k) c= (dom f1) \ {x0} ) by Lm4;
then A8: f1 /* (s ^\ k) is divergent_to+infty by A1, A5, Def2;
A9: rng (s ^\ k) c= (dom f1) /\ (dom f2) by A7, VALUED_1:def 1;
A10: rng s c= dom (f1 + f2) by A3, Lm4;

now

consider r1 being real number such that
A11: for g being set st g in (].(x0 - r),x0.[ \/ ].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 /* (s ^\ k)) . n
let n be Element of NAT ; :: thesis: r2 < (f2 /* (s ^\ k)) . n
k <= n + k by NAT_1:12;
then ( x0 - r < s . (n + k) & s . (n + k) < x0 + r ) by A4;
then ( x0 - r < (s ^\ k) . n & (s ^\ k) . n < x0 + r ) by NAT_1:def 3;
then (s ^\ k) . n in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 + r ) } ;
then A12: (s ^\ k) . n in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
A13: (s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then not (s ^\ k) . n in {x0} by A6, XBOOLE_0:def 5;
then (s ^\ k) . n in ].(x0 - r),(x0 + r).[ \ {x0} by A12, XBOOLE_0:def 5;
then (s ^\ k) . n in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by A2, Th4;
then (s ^\ k) . n in (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) /\ (dom f2) by A7, A13, XBOOLE_0:def 4;
then r1 <= f2 . ((s ^\ k) . n) by A11;
then r1 - 1 < (f2 . ((s ^\ k) . n)) - 0 by XREAL_1:17;
hence r2 < (f2 /* (s ^\ k)) . n by A7, FUNCT_2:185; :: thesis: verum

end;

then f2 /* (s ^\ k) is bounded_below by SEQ_2:def 4;
then A14: (f1 /* (s ^\ k)) + (f2 /* (s ^\ k)) is divergent_to+infty by A8, LIMFUNC1:36;
(f1 /* (s ^\ k)) + (f2 /* (s ^\ k)) = (f1 + f2) /* (s ^\ k) by A9, RFUNCT_2:23
.= ((f1 + f2) /* s) ^\ k by A10, VALUED_0:27 ;
hence (f1 + f2) /* s is divergent_to+infty by A14, LIMFUNC1:34; :: thesis: verum

end;

hence f1 + f2 is_divergent_to+infty_in x0 by A1, Def2; :: thesis: verum