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

proof

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

end;

A8: dom (f | [.a,b.]) = [.a,b.] by A1, RELAT_1:62;
A9: [.a,b.[ c= [.a,b.] by XXREAL_1:24;
].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A10: ].a,b.[ c= dom f by A1;
A11: for r being Real st 0 < r holds
ex s being Real st
( x < s & ( for x1 being Real st x1 < s & x < x1 & x1 in dom f holds
|.((f . x1) - (f . x)).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( x < s & ( for x1 being Real st x1 < s & x < x1 & x1 in dom f holds
|.((f . x1) - (f . x)).| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( x < s & ( for x1 being Real st x1 < s & x < x1 & x1 in dom f holds
|.((f . x1) - (f . x)).| < r ) )
then consider e being Real such that
A12: ( 0 < e & ( for x1 being Real st x1 in dom (f | [.a,b.]) & |.(x1 - x).| < e holds
|.(((f | [.a,b.]) . x1) - ((f | [.a,b.]) . x)).| < r ) ) by A9, A2, A3, A8, FCONT_1:def 2, FCONT_1:3;
set s1 = x + e;
set s = min ((x + e),b);
A13: ( min ((x + e),b) <= x + e & min ((x + e),b) <= b ) by XXREAL_0:17;
A14: x < x + e by A12, XREAL_1:29;
take min ((x + e),b) ; :: thesis: ( x < min ((x + e),b) & ( for x1 being Real st x1 < min ((x + e),b) & x < x1 & x1 in dom f holds
|.((f . x1) - (f . x)).| < r ) )
thus x < min ((x + e),b) by A4, A14, XXREAL_0:21; :: thesis: for x1 being Real st x1 < min ((x + e),b) & x < x1 & x1 in dom f holds
|.((f . x1) - (f . x)).| < r

hereby :: thesis: verum

let x1 be Real; :: thesis: ( x1 < min ((x + e),b) & x < x1 & x1 in dom f implies |.((f . x1) - (f . x)).| < r )
assume that
A15: x1 < min ((x + e),b) and
A16: x < x1 and
x1 in dom f ; :: thesis: |.((f . x1) - (f . x)).| < r
A17: x1 - x < (min ((x + e),b)) - x by A15, XREAL_1:9;
(min ((x + e),b)) - x <= (x + e) - x by XXREAL_0:17, XREAL_1:9;
then A18: x1 - x < (x + e) - x by A17, XXREAL_0:2;
x1 - x > 0 by A16, XREAL_1:50;
then A19: |.(x1 - x).| < e by A18, ABSVALUE:def 1;
a <= x by A9, A3, XXREAL_1:1;
then A20: ( a < x1 & x1 < b ) by A15, A13, A16, XXREAL_0:2;
then A21: x1 in dom (f | [.a,b.]) by A8, XXREAL_1:1;
( (f | [.a,b.]) . x1 = f . x1 & (f | [.a,b.]) . x = f . x ) by A9, A3, A8, A20, XXREAL_1:1, FUNCT_1:47;
hence |.((f . x1) - (f . x)).| < r by A12, A19, A21; :: thesis: verum

end;

end;

hence A22: f is_right_convergent_in x by A5, LIMFUNC2:10; :: thesis: lim_right ((f | ].a,b.[),x) = f . x
A23: for r being Real st 0 < r holds
ex s being Real st
( x < s & ( for x1 being Real st x1 < s & x < x1 & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (f . x)).| < r ) )

proof

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

proof

let x1 be Real; :: thesis: ( x1 < min (s0,b) & x < x1 & x1 in dom (f | ].a,b.[) implies |.(((f | ].a,b.[) . x1) - (f . x)).| < r )
assume that
A25: x1 < min (s0,b) and
A26: x < x1 and
A27: x1 in dom (f | ].a,b.[) ; :: thesis: |.(((f | ].a,b.[) . x1) - (f . x)).| < r
min (s0,b) <= s0 by XXREAL_0:17;
then A28: x1 < s0 by A25, XXREAL_0:2;
x1 in dom f by A27, RELAT_1:57;
then |.((f . x1) - (f . x)).| < r by A24, A28, A26;
hence |.(((f | ].a,b.[) . x1) - (f . x)).| < r by A27, FUNCT_1:47; :: thesis: verum

end;

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

end;

( f | ].a,b.[ is_right_convergent_in x & lim_right ((f | ].a,b.[),x) = lim_right (f,x) ) by A4, A22, A10, Th8;
hence lim_right ((f | ].a,b.[),x) = f . x by A23, LIMFUNC2:42; :: thesis: verum