let p, g be Real; :: thesis: for f being PartFunc of REAL ,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds
for r being Real st r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] holds
ex s being Real st
( s in [.p,g.] & r = f . s )
let f be PartFunc of REAL ,REAL ; :: thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies for r being Real st r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] holds
ex s being Real st
( s in [.p,g.] & r = f . s ) )
assume that
A1: p <= g and
A4: [.p,g.] c= dom f and
X: f | [.p,g.] is continuous ; :: thesis: for r being Real st r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] holds
ex s being Real st
( s in [.p,g.] & r = f . s )
set lb = lower_bound (f .: [.p,g.]);
set ub = upper_bound (f .: [.p,g.]);
let r be Real; :: thesis: ( r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] implies ex s being Real st
( s in [.p,g.] & r = f . s ) )
assume A2: r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] ; :: thesis: ex s being Real st
( s in [.p,g.] & r = f . s )
A3: [.p,g.] <> {} by A1, XXREAL_1:1;
A5: [.p,g.] is compact by RCOMP_1:24;
consider x2, x1 being real number such that
A6: ( x2 in [.p,g.] & x1 in [.p,g.] & f . x2 = upper_bound (f .: [.p,g.]) & f . x1 = lower_bound (f .: [.p,g.]) ) by A3, A4, X, FCONT_1:32, RCOMP_1:24;
reconsider x1 = x1, x2 = x2 as Real by XREAL_0:def 1;
A7: ( f . x1 in f .: [.p,g.] & f . x2 in f .: [.p,g.] ) by A4, A6, FUNCT_1:def 12;
f .: [.p,g.] is bounded by A4, A5, X, FCONT_1:30, RCOMP_1:28;
then A8: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] \/ [.(upper_bound (f .: [.p,g.])),(lower_bound (f .: [.p,g.])).] by A7, SEQ_4:24, XXREAL_1:222;

now

per cases ( x1 <= x2 or x2 <= x1 ) ;

suppose A9: x1 <= x2 ; :: thesis: ex s being Real st
( s in [.p,g.] & r = f . s )

S: [.x1,x2.] c= [.p,g.] by A6, XXREAL_2:def 12;
A10: [.x1,x2.] c= [.p,g.] by A6, XXREAL_2:def 12;
then f | [.x1,x2.] is continuous by X, FCONT_1:17;
then consider s being Real such that
A11: ( s in [.x1,x2.] & r = f . s ) by A2, A6, A8, A9, Th16, S, A4, XBOOLE_1:1;
take s = s; :: thesis: ( s in [.p,g.] & r = f . s )
thus ( s in [.p,g.] & r = f . s ) by A10, A11; :: thesis: verum

end;

suppose A12: x2 <= x1 ; :: thesis: ex s being Real st
( s in [.p,g.] & r = f . s )

[.x2,x1.] c= [.p,g.] by A6, XXREAL_2:def 12;
then T: [.x2,x1.] c= dom f by A4, XBOOLE_1:1;
A13: [.x2,x1.] c= [.p,g.] by A6, XXREAL_2:def 12;
then f | [.x2,x1.] is continuous by X, FCONT_1:17;
then consider s being Real such that
A14: ( s in [.x2,x1.] & r = f . s ) by A2, A6, A8, A12, Th16, T;
take s = s; :: thesis: ( s in [.p,g.] & r = f . s )
thus ( s in [.p,g.] & r = f . s ) by A13, A14; :: thesis: verum

end;

end;

end;

hence ex s being Real st
( s in [.p,g.] & r = f . s ) ; :: thesis: verum