let f, f1, f2 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
( right_open_halfline r c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in right_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 right_open_halfline r c= ((dom f1) /\ (dom f2)) /\ (dom f) or ex g being Real st
( g in right_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: right_open_halfline r1 c= ((dom f1) /\ (dom f2)) /\ (dom f) and
A3: for g being Real st g in right_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 )
((dom f1) /\ (dom f2)) /\ (dom f) c= dom f by XBOOLE_1:17;
then A4: right_open_halfline r1 c= dom f by A2;

A5: now :: thesis: for r being Real ex g being Real st
( r < g & g in dom f )

let r be Real; :: thesis: ex g being Real st
( r < g & g in dom f )
consider g being Real such that
A6: |.r.| + |.r1.| < g by XREAL_1:1;
take g = g; :: thesis: ( r < g & g in dom f )
( r <= |.r.| & 0 <= |.r1.| ) by ABSVALUE:4, COMPLEX1:46;
then r + 0 <= |.r.| + |.r1.| by XREAL_1:7;
hence r < g by A6, XXREAL_0:2; :: thesis: g in dom f
( r1 <= |.r1.| & 0 <= |.r.| ) by ABSVALUE:4, COMPLEX1:46;
then 0 + r1 <= |.r.| + |.r1.| by XREAL_1:7;
then r1 < g by A6, XXREAL_0:2;
then g in { g1 where g1 is Real : r1 < g1 } ;
then g in right_open_halfline r1 by XXREAL_1:230;
hence g in dom f by A4; :: thesis: verum

end;

A7: ((dom f1) /\ (dom f2)) /\ (dom f) c= (dom f1) /\ (dom f2) by XBOOLE_1:17;

now :: thesis: ( (dom f1) /\ (right_open_halfline r1) c= (dom f2) /\ (right_open_halfline r1) & (dom f) /\ (right_open_halfline r1) c= (dom f1) /\ (right_open_halfline r1) & ( for g being Real st g in (dom f) /\ (right_open_halfline r1) holds
( f1 . g <= f . g & f . g <= f2 . g ) ) )

(dom f1) /\ (dom f2) c= dom f1 by XBOOLE_1:17;
then ((dom f1) /\ (dom f2)) /\ (dom f) c= dom f1 by A7;
then A8: (dom f1) /\ (right_open_halfline r1) = right_open_halfline r1 by A2, XBOOLE_1:1, XBOOLE_1:28;
(dom f1) /\ (dom f2) c= dom f2 by XBOOLE_1:17;
then ((dom f1) /\ (dom f2)) /\ (dom f) c= dom f2 by A7;
hence (dom f1) /\ (right_open_halfline r1) c= (dom f2) /\ (right_open_halfline r1) by A2, A8, XBOOLE_1:1, XBOOLE_1:28; :: thesis: ( (dom f) /\ (right_open_halfline r1) c= (dom f1) /\ (right_open_halfline r1) & ( for g being Real st g in (dom f) /\ (right_open_halfline r1) holds
( f1 . g <= f . g & f . g <= f2 . g ) ) )
thus (dom f) /\ (right_open_halfline r1) c= (dom f1) /\ (right_open_halfline r1) by A8, XBOOLE_1:17; :: thesis: for g being Real st g in (dom f) /\ (right_open_halfline r1) holds
( f1 . g <= f . g & f . g <= f2 . g )
let g be Real; :: thesis: ( g in (dom f) /\ (right_open_halfline r1) implies ( f1 . g <= f . g & f . g <= f2 . g ) )
assume g in (dom f) /\ (right_open_halfline r1) ; :: thesis: ( f1 . g <= f . g & f . g <= f2 . g )
then g in right_open_halfline r1 by XBOOLE_0:def 4;
hence ( f1 . g <= f . g & f . g <= f2 . g ) by A3; :: thesis: verum

end;

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