let a, b, x be Real; :: thesis: for f being PartFunc of REAL,REAL st a <= x & x < b & ].a,b.[ c= dom f & f is_right_convergent_in x holds
( f | ].a,b.[ is_right_convergent_in x & lim_right ((f | ].a,b.[),x) = lim_right (f,x) )
let f be PartFunc of REAL,REAL; :: thesis: ( a <= x & x < b & ].a,b.[ c= dom f & f is_right_convergent_in x implies ( f | ].a,b.[ is_right_convergent_in x & lim_right ((f | ].a,b.[),x) = lim_right (f,x) ) )
assume that
A1: ( a <= x & x < b ) and
A2: ].a,b.[ c= dom f and
A3: f is_right_convergent_in x ; :: thesis: ( f | ].a,b.[ is_right_convergent_in x & lim_right ((f | ].a,b.[),x) = lim_right (f,x) )
A4: dom (f | ].a,b.[) = ].a,b.[ by A2, RELAT_1:62;
A5: for r being Real st x < r holds
ex g being Real st
( g < r & x < g & g in dom (f | ].a,b.[) )

proof

let r be Real; :: thesis: ( x < r implies ex g being Real st
( g < r & x < g & g in dom (f | ].a,b.[) ) )
assume A6: x < r ; :: thesis: ex g being Real st
( g < r & x < g & g in dom (f | ].a,b.[) )
set s = min (r,b);
consider g being Real such that
A7: ( x < g & g < min (r,b) ) by A6, A1, XXREAL_0:21, XREAL_1:5;
A8: ( min (r,b) <= r & min (r,b) <= b ) by XXREAL_0:17;
then A9: g < r by A7, XXREAL_0:2;
( a < g & g < b ) by A1, A7, A8, XXREAL_0:2;
hence ex g being Real st
( g < r & x < g & g in dom (f | ].a,b.[) ) by A7, A9, A4, XXREAL_1:4; :: thesis: verum

end;

A10: for r being Real st 0 < r holds
ex d being Real st
( x < d & ( for x1 being Real st x1 < d & x < x1 & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (lim_right (f,x))).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex d being Real st
( x < d & ( for x1 being Real st x1 < d & x < x1 & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (lim_right (f,x))).| < r ) ) )
assume 0 < r ; :: thesis: ex d being Real st
( x < d & ( for x1 being Real st x1 < d & x < x1 & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (lim_right (f,x))).| < r ) )
then consider d0 being Real such that
A11: ( x < d0 & ( for x1 being Real st x1 < d0 & x < x1 & x1 in dom f holds
|.((f . x1) - (lim_right (f,x))).| < r ) ) by A3, LIMFUNC2:42;
set d = min (d0,b);
for x1 being Real st x1 < min (d0,b) & x < x1 & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (lim_right (f,x))).| < r

proof

let x1 be Real; :: thesis: ( x1 < min (d0,b) & x < x1 & x1 in dom (f | ].a,b.[) implies |.(((f | ].a,b.[) . x1) - (lim_right (f,x))).| < r )
assume that
A12: x1 < min (d0,b) and
A13: x < x1 and
A14: x1 in dom (f | ].a,b.[) ; :: thesis: |.(((f | ].a,b.[) . x1) - (lim_right (f,x))).| < r
min (d0,b) <= d0 by XXREAL_0:17;
then A15: x1 < d0 by A12, XXREAL_0:2;
x1 in dom f by A14, RELAT_1:57;
then |.((f . x1) - (lim_right (f,x))).| < r by A15, A13, A11;
hence |.(((f | ].a,b.[) . x1) - (lim_right (f,x))).| < r by A14, FUNCT_1:47; :: thesis: verum

end;

hence ex d being Real st
( x < d & ( for x1 being Real st x1 < d & x < x1 & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (lim_right (f,x))).| < r ) ) by A11, A1, XXREAL_0:21; :: thesis: verum

end;

hence f | ].a,b.[ is_right_convergent_in x by A5, LIMFUNC2:10; :: thesis: lim_right ((f | ].a,b.[),x) = lim_right (f,x)
hence lim_right ((f | ].a,b.[),x) = lim_right (f,x) by A10, LIMFUNC2:42; :: thesis: verum