let f1, f 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 f ) ) & ex r being Real st
( (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f1 . g <= f . g ) ) implies f 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 f ) ) ) ; :: thesis: ( for r being Real holds
( not (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) or ex g being Real st
( g in (dom f) /\ (left_open_halfline r) & not f1 . g <= f . g ) ) or f is divergent_in-infty_to+infty )
given r1 being Real such that A2: ( (dom f) /\ (left_open_halfline r1) c= (dom f1) /\ (left_open_halfline r1) & ( for g being Real st g in (dom f) /\ (left_open_halfline r1) holds
f1 . g <= f . g ) ) ; :: thesis: f is divergent_in-infty_to+infty

now

let seq be Real_Sequence; :: thesis: ( seq is divergent_to-infty & rng seq c= dom f implies f /* seq is divergent_to+infty )
assume A3: ( seq is divergent_to-infty & rng seq c= dom f ) ; :: thesis: f /* seq is divergent_to+infty
then consider k being Element of NAT such that
A4: for n being Element of NAT st k <= n holds
seq . n < r1 by Def5;
A5: rng (seq ^\ k) c= rng seq by VALUED_0:21;
then A6: rng (seq ^\ k) c= dom f by A3, XBOOLE_1:1;

now

let x be set ; :: thesis: ( x in rng (seq ^\ k) implies x in left_open_halfline r1 )
assume x in rng (seq ^\ k) ; :: thesis: x in left_open_halfline r1
then consider n being Element of NAT such that
A7: (seq ^\ k) . n = x by FUNCT_2:190;
seq . (n + k) < r1 by A4, NAT_1:12;
then (seq ^\ k) . n < r1 by NAT_1:def 3;
then x in { g2 where g2 is Real : g2 < r1 } by A7;
hence x in left_open_halfline r1 by XXREAL_1:229; :: thesis: verum

end;

then rng (seq ^\ k) c= left_open_halfline r1 by TARSKI:def 3;
then A8: rng (seq ^\ k) c= (dom f) /\ (left_open_halfline r1) by A6, XBOOLE_1:19;
then A9: rng (seq ^\ k) c= (dom f1) /\ (left_open_halfline r1) by A2, XBOOLE_1:1;
A10: (dom f1) /\ (left_open_halfline r1) c= dom f1 by XBOOLE_1:17;
then A11: rng (seq ^\ k) c= dom f1 by A9, XBOOLE_1:1;
seq ^\ k is divergent_to-infty by A3, Th54;
then A12: f1 /* (seq ^\ k) is divergent_to+infty by A1, A11, Def10;

now

let n be Element of NAT ; :: thesis: (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n
(seq ^\ k) . n in rng (seq ^\ k) by VALUED_0:28;
then f1 . ((seq ^\ k) . n) <= f . ((seq ^\ k) . n) by A2, A8;
then (f1 /* (seq ^\ k)) . n <= f . ((seq ^\ k) . n) by A9, A10, FUNCT_2:185, XBOOLE_1:1;
hence (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n by A3, A5, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

then A13: f /* (seq ^\ k) is divergent_to+infty by A12, Th69;
f /* (seq ^\ k) = (f /* seq) ^\ k by A3, VALUED_0:27;
hence f /* seq is divergent_to+infty by A13, Th34; :: thesis: verum

end;

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