let f1, f be PartFunc of REAL ,REAL ; :: thesis: ( f1 is divergent_in-infty_to-infty & ex r being Real st
( left_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in left_open_halfline r holds
f . g <= f1 . g ) ) implies f is divergent_in-infty_to-infty )
assume A1: f1 is divergent_in-infty_to-infty ; :: thesis: ( for r being Real holds
( not left_open_halfline r c= (dom f) /\ (dom f1) or ex g being Real st
( g in left_open_halfline r & not f . g <= f1 . g ) ) or f is divergent_in-infty_to-infty )
given r1 being Real such that A2: left_open_halfline r1 c= (dom f) /\ (dom f1) and
A3: for g being Real st g in left_open_halfline r1 holds
f . g <= f1 . g ; :: thesis: f is divergent_in-infty_to-infty

A4: now

let r be Real; :: thesis: ex g being Real st
( g < r & g in dom f )
consider g being real number such that
A5: g < (- (abs r)) - (abs r1) by XREAL_1:4;
reconsider g = g as Real by XREAL_0:def 1;
take g = g; :: thesis: ( g < r & g in dom f )
( 0 <= abs r1 & - (abs r) <= r ) by ABSVALUE:11, COMPLEX1:132;
then (- (abs r)) - (abs r1) <= r - 0 by XREAL_1:15;
hence g < r by A5, XXREAL_0:2; :: thesis: g in dom f
( 0 <= abs r & - (abs r1) <= r1 ) by ABSVALUE:11, COMPLEX1:132;
then (- (abs r1)) - (abs r) <= r1 - 0 by XREAL_1:15;
then g < r1 by A5, XXREAL_0:2;
then g in { g2 where g2 is Real : g2 < r1 } ;
then g in left_open_halfline r1 by XXREAL_1:229;
hence g in dom f by A2, XBOOLE_0:def 4; :: thesis: verum

end;

now

(dom f) /\ (dom f1) c= dom f by XBOOLE_1:17;
then A6: (dom f) /\ (left_open_halfline r1) = left_open_halfline r1 by A2, XBOOLE_1:1, XBOOLE_1:28;
(dom f) /\ (dom f1) c= dom f1 by XBOOLE_1:17;
hence (dom f) /\ (left_open_halfline r1) c= (dom f1) /\ (left_open_halfline r1) by A2, A6, XBOOLE_1:1, XBOOLE_1:28; :: thesis: for g being Real st g in (dom f) /\ (left_open_halfline r1) holds
f . g <= f1 . g
let g be Real; :: thesis: ( g in (dom f) /\ (left_open_halfline r1) implies f . g <= f1 . g )
assume g in (dom f) /\ (left_open_halfline r1) ; :: thesis: f . g <= f1 . g
hence f . g <= f1 . g by A3, A6; :: thesis: verum

end;

hence f is divergent_in-infty_to-infty by A1, A4, Th106; :: thesis: verum