let f1, f2, f be PartFunc of REAL ,REAL ; :: thesis: ( f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f1 = lim_in-infty f2 & ex r being Real st
( left_open_halfline r c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in left_open_halfline r holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) implies ( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 ) )
assume A1: ( f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f1 = lim_in-infty f2 ) ; :: thesis: ( for r being Real holds
( not left_open_halfline r c= ((dom f1) /\ (dom f2)) /\ (dom f) or ex g being Real st
( g in left_open_halfline r & not ( f1 . g <= f . g & f . g <= f2 . g ) ) ) or ( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 ) )
given r1 being Real such that A2: ( left_open_halfline r1 c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in left_open_halfline r1 holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) ; :: thesis: ( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 )
A3: ( ((dom f1) /\ (dom f2)) /\ (dom f) c= dom f & ((dom f1) /\ (dom f2)) /\ (dom f) c= (dom f1) /\ (dom f2) ) by XBOOLE_1:17;
then A4: left_open_halfline r1 c= dom f by A2, XBOOLE_1:1;

A5: now

let r be Real; :: thesis: ex g being Real st
( g < r & g in dom f )
consider g being real number such that
A6: 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 )
A7: - (abs r) <= r by ABSVALUE:11;
0 <= abs r1 by COMPLEX1:132;
then (- (abs r)) - (abs r1) <= r - 0 by A7, XREAL_1:15;
hence g < r by A6, XXREAL_0:2; :: thesis: g in dom f
A8: - (abs r1) <= r1 by ABSVALUE:11;
0 <= abs r by COMPLEX1:132;
then (- (abs r1)) - (abs r) <= r1 - 0 by A8, XREAL_1:15;
then g < r1 by A6, XXREAL_0:2;
then g in { g1 where g1 is Real : g1 < r1 } ;
then g in left_open_halfline r1 by XXREAL_1:229;
hence g in dom f by A4; :: thesis: verum

end;

now

( (dom f1) /\ (dom f2) c= dom f1 & (dom f1) /\ (dom f2) c= dom f2 ) by XBOOLE_1:17;
then X: ( ((dom f1) /\ (dom f2)) /\ (dom f) c= dom f1 & ((dom f1) /\ (dom f2)) /\ (dom f) c= dom f2 ) by A3, XBOOLE_1:1;
A10: (dom f1) /\ (left_open_halfline r1) = left_open_halfline r1 by X, A2, XBOOLE_1:1, XBOOLE_1:28;
hence (dom f1) /\ (left_open_halfline r1) c= (dom f2) /\ (left_open_halfline r1) by X, A2, XBOOLE_1:1, XBOOLE_1:28; :: thesis: ( (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 & f . g <= f2 . g ) ) )
thus (dom f) /\ (left_open_halfline r1) c= (dom f1) /\ (left_open_halfline r1) by A3, A10, A2, XBOOLE_1:1, XBOOLE_1:28; :: thesis: for g being Real st g in (dom f) /\ (left_open_halfline r1) holds
( f1 . g <= f . g & f . g <= f2 . g )
let g be Real; :: thesis: ( g in (dom f) /\ (left_open_halfline r1) implies ( f1 . g <= f . g & f . g <= f2 . g ) )
assume g in (dom f) /\ (left_open_halfline r1) ; :: thesis: ( f1 . g <= f . g & f . g <= f2 . g )
then g in left_open_halfline r1 by XBOOLE_0:def 4;
hence ( f1 . g <= f . g & f . g <= f2 . g ) by A2; :: thesis: verum

end;

hence ( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 ) by A1, A5, Th137; :: thesis: verum