let x0 be Real; :: thesis: for f, f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & lim_right (f1,x0) = lim_right (f2,x0) & ex r being Real st
( 0 < r & ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].x0,(x0 + r).[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )
let f, f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & lim_right (f1,x0) = lim_right (f2,x0) & ex r being Real st
( 0 < r & ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].x0,(x0 + r).[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) implies ( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) ) )
assume that
A1: f1 is_right_convergent_in x0 and
A2: f2 is_right_convergent_in x0 and
A3: lim_right (f1,x0) = lim_right (f2,x0) ; :: thesis: ( for r being Real holds
( not 0 < r or not ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) or ex g being Real st
( g in ].x0,(x0 + r).[ & not ( f1 . g <= f . g & f . g <= f2 . g ) ) ) or ( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) ) )
given r being Real such that A4: 0 < r and
A5: ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) and
A6: for g being Real st g in ].x0,(x0 + r).[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ; :: thesis: ( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )
((dom f1) /\ (dom f2)) /\ (dom f) c= (dom f1) /\ (dom f2) by XBOOLE_1:17;
then A7: ].x0,(x0 + r).[ c= (dom f1) /\ (dom f2) by A5, XBOOLE_1:1;
A8: ((dom f1) /\ (dom f2)) /\ (dom f) c= dom f by XBOOLE_1:17;
then A9: ].x0,(x0 + r).[ c= dom f by A5, XBOOLE_1:1;

A10: now :: thesis: for r1 being Real st x0 < r1 holds
ex g being Real st
( g < r1 & x0 < g & g in dom f )

let r1 be Real; :: thesis: ( x0 < r1 implies ex g being Real st
( g < r1 & x0 < g & g in dom f ) )
assume A11: x0 < r1 ; :: thesis: ex g being Real st
( g < r1 & x0 < g & g in dom f )

now :: thesis: ex g being Real st
( g < r1 & x0 < g & g in dom f )

per cases ( r1 <= x0 + r or x0 + r <= r1 ) ;

suppose A12: r1 <= x0 + r ; :: thesis: ex g being Real st
( g < r1 & x0 < g & g in dom f )

now :: thesis: ex g being Real st
( g < r1 & x0 < g & g in dom f )

consider g being Real such that
A13: x0 < g and
A14: g < r1 by A11, XREAL_1:5;
reconsider g = g as Real ;
take g = g; :: thesis: ( g < r1 & x0 < g & g in dom f )
thus ( g < r1 & x0 < g ) by A13, A14; :: thesis: g in dom f
g < x0 + r by A12, A14, XXREAL_0:2;
then g in { g2 where g2 is Real : ( x0 < g2 & g2 < x0 + r ) } by A13;
then g in ].x0,(x0 + r).[ by RCOMP_1:def 2;
hence g in dom f by A9; :: thesis: verum

end;

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

end;

suppose A15: x0 + r <= r1 ; :: thesis: ex g being Real st
( g < r1 & x0 < g & g in dom f )

now :: thesis: ex g being Real st
( g < r1 & x0 < g & g in dom f )

x0 + 0 < x0 + r by A4, XREAL_1:8;
then consider g being Real such that
A16: x0 < g and
A17: g < x0 + r by XREAL_1:5;
reconsider g = g as Real ;
take g = g; :: thesis: ( g < r1 & x0 < g & g in dom f )
thus ( g < r1 & x0 < g ) by A15, A16, A17, XXREAL_0:2; :: thesis: g in dom f
g in { g2 where g2 is Real : ( x0 < g2 & g2 < x0 + r ) } by A16, A17;
then g in ].x0,(x0 + r).[ by RCOMP_1:def 2;
hence g in dom f by A9; :: thesis: verum

end;

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

end;

end;

end;

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

end;

(dom f1) /\ (dom f2) c= dom f2 by XBOOLE_1:17;
then A18: (dom f2) /\ ].x0,(x0 + r).[ = ].x0,(x0 + r).[ by A7, XBOOLE_1:1, XBOOLE_1:28;
(dom f1) /\ (dom f2) c= dom f1 by XBOOLE_1:17;
then A19: (dom f1) /\ ].x0,(x0 + r).[ = ].x0,(x0 + r).[ by A7, XBOOLE_1:1, XBOOLE_1:28;
(dom f) /\ ].x0,(x0 + r).[ = ].x0,(x0 + r).[ by A5, A8, XBOOLE_1:1, XBOOLE_1:28;
hence ( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) ) by A1, A2, A3, A4, A6, A19, A18, A10, Th65; :: thesis: verum