let f be PartFunc of REAL ,REAL ; :: thesis: ( f is convergent_in-infty & lim_in-infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f . g < 0 implies f ^ is divergent_in-infty_to-infty )
assume A1: ( f is convergent_in-infty & lim_in-infty f = 0 ) ; :: thesis: ( for r being Real ex g being Real st
( g in (dom f) /\ (left_open_halfline r) & not f . g < 0 ) or f ^ is divergent_in-infty_to-infty )
given r being Real such that A2: for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f . g < 0 ; :: thesis: f ^ is divergent_in-infty_to-infty
thus for r1 being Real ex g1 being Real st
( g1 < r1 & g1 in dom (f ^ ) ) :: according to LIMFUNC1:def 11 :: thesis: for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom (f ^ ) holds
(f ^ ) /* seq is divergent_to-infty

proof

let r1 be Real; :: thesis: ex g1 being Real st
( g1 < r1 & g1 in dom (f ^ ) )
consider g1 being Real such that
A3: ( g1 < r1 & g1 in dom f ) by A1, Def9;

now

per cases ( g1 <= r or r <= g1 ) ;

suppose A4: g1 <= r ; :: thesis: ex g2 being Real st
( g2 < r1 & g2 in dom (f ^ ) )

consider g2 being Real such that
A5: ( g2 < g1 & g2 in dom f ) by A1, Def9;
take g2 = g2; :: thesis: ( g2 < r1 & g2 in dom (f ^ ) )
thus g2 < r1 by A3, A5, XXREAL_0:2; :: thesis: g2 in dom (f ^ )
g2 < r by A4, A5, XXREAL_0:2;
then g2 in { r2 where r2 is Real : r2 < r } ;
then g2 in left_open_halfline r by XXREAL_1:229;
then g2 in (dom f) /\ (left_open_halfline r) by A5, XBOOLE_0:def 4;
then 0 <> f . g2 by A2;
then not f . g2 in {0 } by TARSKI:def 1;
then not g2 in f " {0 } by FUNCT_1:def 13;
then g2 in (dom f) \ (f " {0 }) by A5, XBOOLE_0:def 5;
hence g2 in dom (f ^ ) by RFUNCT_1:def 8; :: thesis: verum

end;

suppose A6: r <= g1 ; :: thesis: ex g2 being Real st
( g2 < r1 & g2 in dom (f ^ ) )

consider g2 being Real such that
A7: ( g2 < r & g2 in dom f ) by A1, Def9;
take g2 = g2; :: thesis: ( g2 < r1 & g2 in dom (f ^ ) )
g2 < g1 by A6, A7, XXREAL_0:2;
hence g2 < r1 by A3, XXREAL_0:2; :: thesis: g2 in dom (f ^ )
g2 in { r2 where r2 is Real : r2 < r } by A7;
then g2 in left_open_halfline r by XXREAL_1:229;
then g2 in (dom f) /\ (left_open_halfline r) by A7, XBOOLE_0:def 4;
then 0 <> f . g2 by A2;
then not f . g2 in {0 } by TARSKI:def 1;
then not g2 in f " {0 } by FUNCT_1:def 13;
then g2 in (dom f) \ (f " {0 }) by A7, XBOOLE_0:def 5;
hence g2 in dom (f ^ ) by RFUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence ex g1 being Real st
( g1 < r1 & g1 in dom (f ^ ) ) ; :: thesis: verum

end;

let s be Real_Sequence; :: thesis: ( s is divergent_to-infty & rng s c= dom (f ^ ) implies (f ^ ) /* s is divergent_to-infty )
assume A8: ( s is divergent_to-infty & rng s c= dom (f ^ ) ) ; :: thesis: (f ^ ) /* s is divergent_to-infty
then consider k being Element of NAT such that
A9: for n being Element of NAT st k <= n holds
s . n < r by Def5;
A10: s ^\ k is divergent_to-infty by A8, Th54;
dom (f ^ ) = (dom f) \ (f " {0 }) by RFUNCT_1:def 8;
then A11: dom (f ^ ) c= dom f by XBOOLE_1:36;
then A12: rng s c= dom f by A8, XBOOLE_1:1;
A13: rng (s ^\ k) c= rng s by VALUED_0:21;
then A14: ( rng (s ^\ k) c= dom (f ^ ) & rng (s ^\ k) c= dom f ) by A8, A12, XBOOLE_1:1;
then A15: ( f /* (s ^\ k) is convergent & lim (f /* (s ^\ k)) = 0 ) by A1, A10, Def13;

A16: now

let n be Element of NAT ; :: thesis: (f /* (s ^\ k)) . n < 0
A17: (s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
s . (n + k) < r by A9, NAT_1:12;
then (s ^\ k) . n < r by NAT_1:def 3;
then (s ^\ k) . n in { g2 where g2 is Real : g2 < r } ;
then (s ^\ k) . n in left_open_halfline r by XXREAL_1:229;
then (s ^\ k) . n in (dom f) /\ (left_open_halfline r) by A14, A17, XBOOLE_0:def 4;
then f . ((s ^\ k) . n) < 0 by A2;
hence (f /* (s ^\ k)) . n < 0 by A12, A13, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

then for n being Element of NAT holds 0 <> (f /* (s ^\ k)) . n ;
then A18: f /* (s ^\ k) is non-zero by SEQ_1:7;
for n being Element of NAT st 0 <= n holds
(f /* (s ^\ k)) . n < 0 by A16;
then A19: (f /* (s ^\ k)) " is divergent_to-infty by A15, A18, Th63;
(f /* (s ^\ k)) " = ((f /* s) ^\ k) " by A8, A11, VALUED_0:27, XBOOLE_1:1
.= ((f /* s) " ) ^\ k by SEQM_3:41
.= ((f ^ ) /* s) ^\ k by A8, RFUNCT_2:27 ;
hence (f ^ ) /* s is divergent_to-infty by A19, Th34; :: thesis: verum