let a, b, x be Real; :: thesis: for f being PartFunc of REAL,REAL
for I being Interval st inf I <= a & b <= sup I & I c= dom f & f | I is continuous & x in ].a,b.[ holds
f is_continuous_in x
let f be PartFunc of REAL,REAL; :: thesis: for I being Interval st inf I <= a & b <= sup I & I c= dom f & f | I is continuous & x in ].a,b.[ holds
f is_continuous_in x
let I be Interval; :: thesis: ( inf I <= a & b <= sup I & I c= dom f & f | I is continuous & x in ].a,b.[ implies f is_continuous_in x )
assume that
A1: inf I <= a and
A2: b <= sup I and
A3: I c= dom f and
A4: f | I is continuous and
A5: x in ].a,b.[ ; :: thesis: f is_continuous_in x
A6: ].(inf I),(sup I).[ c= I by FDIFF_12:2;
A7: ].a,b.[ c= ].(inf I),(sup I).[ by A1, A2, XXREAL_1:46;
then ].a,b.[ c= I by A6;
then A8: f | ].a,b.[ is continuous by A4, FCONT_1:16;
].a,b.[ c= dom f by A7, A6, A3;
then A9: ].a,b.[ c= dom (f | ].a,b.[) by RELAT_1:62;

now :: thesis: for r being Real st 0 < r holds
ex s being object st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x).| < s holds
|.((f . x1) - (f . x)).| < r ) )

let r be Real; :: thesis: ( 0 < r implies ex s being object st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x).| < s holds
|.((f . x1) - (f . x)).| < r ) ) )
assume 0 < r ; :: thesis: ex s being object st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x).| < s holds
|.((f . x1) - (f . x)).| < r ) )
then consider s1 being Real such that
A10: ( 0 < s1 & ( for x1 being Real st x1 in dom (f | ].a,b.[) & |.(x1 - x).| < s1 holds
|.(((f | ].a,b.[) . x1) - ((f | ].a,b.[) . x)).| < r ) ) by A8, A5, A9, FCONT_1:def 2, FCONT_1:3;
( a < x & x < b ) by A5, XXREAL_1:4;
then A11: ( 0 < x - a & 0 < b - x ) by XREAL_1:50;
then A12: ( 0 < (x - a) / 2 & 0 < (b - x) / 2 ) by XREAL_1:215;
set s2 = min (((x - a) / 2),((b - x) / 2));
A13: 0 < min (((x - a) / 2),((b - x) / 2)) by A12, XXREAL_0:21;
take s = min (s1,(min (((x - a) / 2),((b - x) / 2)))); :: thesis: ( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x).| < s holds
|.((f . x1) - (f . x)).| < r ) )
thus 0 < s by A10, A13, XXREAL_0:21; :: thesis: for x1 being Real st x1 in dom f & |.(x1 - x).| < s holds
|.((f . x1) - (f . x)).| < r
A14: ( (x - a) / 2 < x - a & (b - x) / 2 < b - x ) by A11, XREAL_1:216;
( min (((x - a) / 2),((b - x) / 2)) <= (x - a) / 2 & min (((x - a) / 2),((b - x) / 2)) <= (b - x) / 2 ) by XXREAL_0:17;
then A15: ( min (((x - a) / 2),((b - x) / 2)) < x - a & min (((x - a) / 2),((b - x) / 2)) < b - x ) by A14, XXREAL_0:2;
A16: ( s <= s1 & s <= min (((x - a) / 2),((b - x) / 2)) ) by XXREAL_0:17;
then ( s < x - a & s < b - x ) by A15, XXREAL_0:2;
then A17: ( a < x - s & x + s < b ) by XREAL_1:12, XREAL_1:20;
thus for x1 being Real st x1 in dom f & |.(x1 - x).| < s holds
|.((f . x1) - (f . x)).| < r :: thesis: verum

proof

let x1 be Real; :: thesis: ( x1 in dom f & |.(x1 - x).| < s implies |.((f . x1) - (f . x)).| < r )
assume that
x1 in dom f and
A18: |.(x1 - x).| < s ; :: thesis: |.((f . x1) - (f . x)).| < r
A19: ( - |.(x1 - x).| <= x1 - x & x1 - x <= |.(x1 - x).| ) by ABSVALUE:4;
then x1 - x < s by A18, XXREAL_0:2;
then x1 < x + s by XREAL_1:19;
then A20: x1 < b by A17, XXREAL_0:2;
- (x1 - x) <= |.(x1 - x).| by A19, XREAL_1:26;
then x - x1 < s by A18, XXREAL_0:2;
then x < s + x1 by XREAL_1:19;
then x - s < x1 by XREAL_1:19;
then a < x1 by A17, XXREAL_0:2;
then A21: x1 in dom (f | ].a,b.[) by A9, A20, XXREAL_1:4;
then A22: ( (f | ].a,b.[) . x1 = f . x1 & (f | ].a,b.[) . x = f . x ) by A5, A9, FUNCT_1:47;
|.(x1 - x).| < s1 by A18, A16, XXREAL_0:2;
hence |.((f . x1) - (f . x)).| < r by A10, A21, A22; :: thesis: verum

end;

end;

hence f is_continuous_in x by FCONT_1:3; :: thesis: verum