let a, b, d be Real; :: thesis: for f being PartFunc of REAL,REAL st a < b & [.a,b.] c= dom f & f | [.a,b.] is continuous & f . a < d & d < f . b holds
ex c being Real st
( a < c & c < b & d = f . c )
let f be PartFunc of REAL,REAL; :: thesis: ( a < b & [.a,b.] c= dom f & f | [.a,b.] is continuous & f . a < d & d < f . b implies ex c being Real st
( a < c & c < b & d = f . c ) )
assume A1: ( a < b & [.a,b.] c= dom f & f | [.a,b.] is continuous & f . a < d & d < f . b ) ; :: thesis: ex c being Real st
( a < c & c < b & d = f . c )
A2: dom (f | [.a,b.]) = [.a,b.] by A1, RELAT_1:62;
A3: [.a,b.] = the carrier of (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18;
rng (f | [.a,b.]) c= the carrier of R^1 by TOPMETR:17;
then reconsider g = f | [.a,b.] as Function of (Closed-Interval-TSpace (a,b)),R^1 by A2, A3, FUNCT_2:2;
( a in [.a,b.] & b in [.a,b.] ) by A1;
then A4: ( g . a = f . a & g . b = f . b ) by FUNCT_1:49;
set T = Closed-Interval-TSpace (a,b);
for p being Point of (Closed-Interval-TSpace (a,b))
for r being positive Real ex W being open Subset of (Closed-Interval-TSpace (a,b)) st
( p in W & g .: W c= ].((g . p) - r),((g . p) + r).[ )

proof

let p be Point of (Closed-Interval-TSpace (a,b)); :: thesis: for r being positive Real ex W being open Subset of (Closed-Interval-TSpace (a,b)) st
( p in W & g .: W c= ].((g . p) - r),((g . p) + r).[ )
let r be positive Real; :: thesis: ex W being open Subset of (Closed-Interval-TSpace (a,b)) st
( p in W & g .: W c= ].((g . p) - r),((g . p) + r).[ )
reconsider q = p as Real ;
consider s being Real such that
A7: ( 0 < s & ( for t being Real st t in [.a,b.] & |.(t - q).| < s holds
|.((f . t) - (f . q)).| < r ) ) by A1, A3, FCONT_1:14;
reconsider W0 = ].(q - s),(q + s).[ as open Subset of R^1 by BORSUK_5:39, TOPMETR:17;
reconsider P = [.a,b.] as Subset of R^1 by TOPMETR:17;
reconsider W = W0 /\ [.a,b.] as Subset of (Closed-Interval-TSpace (a,b)) by A3, XBOOLE_1:17;
[.a,b.] = [#] (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18;
then reconsider W = W as open Subset of (Closed-Interval-TSpace (a,b)) by TOPS_2:24;
take W ; :: thesis: ( p in W & g .: W c= ].((g . p) - r),((g . p) + r).[ )
|.(q - q).| = 0 by COMPLEX1:44;
then q in ].(q - s),(q + s).[ by A7, RCOMP_1:1;
hence p in W by A3, XBOOLE_0:def 4; :: thesis: g .: W c= ].((g . p) - r),((g . p) + r).[

now :: thesis: for z being object st z in g .: W holds
z in ].((g . p) - r),((g . p) + r).[

let z be object ; :: thesis: ( z in g .: W implies z in ].((g . p) - r),((g . p) + r).[ )
assume z in g .: W ; :: thesis: z in ].((g . p) - r),((g . p) + r).[
then consider x being object such that
A9: ( x in dom g & x in W & z = g . x ) by FUNCT_1:def 6;
A10: ( x in ].(q - s),(q + s).[ & x in [.a,b.] ) by A9, XBOOLE_0:def 4;
reconsider x = x as Real by A9;
|.(x - q).| < s by A10, RCOMP_1:1;
then A11: |.((f . x) - (f . q)).| < r by A7, A10;
( f . x = g . x & f . q = g . p ) by A3, A9, FUNCT_1:49;
hence z in ].((g . p) - r),((g . p) + r).[ by A9, A11, RCOMP_1:1; :: thesis: verum

end;

hence g .: W c= ].((g . p) - r),((g . p) + r).[ ; :: thesis: verum

end;

then g is continuous by TOPS_4:21;
then consider c being Real such that
A12: ( g . c = d & a < c & c < b ) by A1, A4, TOPREAL5:6;
take c ; :: thesis: ( a < c & c < b & d = f . c )
c in [.a,b.] by A12;
hence ( a < c & c < b & d = f . c ) by A12, FUNCT_1:49; :: thesis: verum