let g, p 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

A2: [.p,g.] c= dom f and

A3: 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 )

[.p,g.] is compact by RCOMP_1:6;

then A4: f .: [.p,g.] is real-bounded by A2, A3, FCONT_1:29, RCOMP_1:10;

set ub = upper_bound (f .: [.p,g.]);

set lb = lower_bound (f .: [.p,g.]);

[.p,g.] <> {} by A1, XXREAL_1:1;

then consider x2, x1 being Real such that

A5: x2 in [.p,g.] and

A6: x1 in [.p,g.] and

A7: f . x2 = upper_bound (f .: [.p,g.]) and

A8: f . x1 = lower_bound (f .: [.p,g.]) by A2, A3, FCONT_1:31, RCOMP_1:6;

reconsider x1 = x1, x2 = x2 as Real ;

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 A9: 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 )

f . x1 in f .: [.p,g.] by A2, A6, FUNCT_1:def 6;

then A10: [.(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 A4, SEQ_4:11, XXREAL_1:222;

( s in [.p,g.] & r = f . s ) ; :: thesis: verum

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

A2: [.p,g.] c= dom f and

A3: 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 )

[.p,g.] is compact by RCOMP_1:6;

then A4: f .: [.p,g.] is real-bounded by A2, A3, FCONT_1:29, RCOMP_1:10;

set ub = upper_bound (f .: [.p,g.]);

set lb = lower_bound (f .: [.p,g.]);

[.p,g.] <> {} by A1, XXREAL_1:1;

then consider x2, x1 being Real such that

A5: x2 in [.p,g.] and

A6: x1 in [.p,g.] and

A7: f . x2 = upper_bound (f .: [.p,g.]) and

A8: f . x1 = lower_bound (f .: [.p,g.]) by A2, A3, FCONT_1:31, RCOMP_1:6;

reconsider x1 = x1, x2 = x2 as Real ;

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 A9: 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 )

f . x1 in f .: [.p,g.] by A2, A6, FUNCT_1:def 6;

then A10: [.(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 A4, SEQ_4:11, XXREAL_1:222;

now :: thesis: ex s being Real st

( s in [.p,g.] & r = f . s )end;

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

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

end;

suppose A11:
x1 <= x2
; :: thesis: ex s being Real st

( s in [.p,g.] & r = f . s )

( s in [.p,g.] & r = f . s )

A12:
[.x1,x2.] c= [.p,g.]
by A5, A6, XXREAL_2:def 12;

A13: [.x1,x2.] c= [.p,g.] by A5, A6, XXREAL_2:def 12;

then f | [.x1,x2.] is continuous by A3, FCONT_1:16;

then consider s being Real such that

A14: s in [.x1,x2.] and

A15: r = f . s by A2, A9, A7, A8, A10, A11, A12, Th15, XBOOLE_1:1;

take s = s; :: thesis: ( s in [.p,g.] & r = f . s )

thus ( s in [.p,g.] & r = f . s ) by A13, A14, A15; :: thesis: verum

end;A13: [.x1,x2.] c= [.p,g.] by A5, A6, XXREAL_2:def 12;

then f | [.x1,x2.] is continuous by A3, FCONT_1:16;

then consider s being Real such that

A14: s in [.x1,x2.] and

A15: r = f . s by A2, A9, A7, A8, A10, A11, A12, Th15, XBOOLE_1:1;

take s = s; :: thesis: ( s in [.p,g.] & r = f . s )

thus ( s in [.p,g.] & r = f . s ) by A13, A14, A15; :: thesis: verum

suppose A16:
x2 <= x1
; :: thesis: ex s being Real st

( s in [.p,g.] & r = f . s )

( s in [.p,g.] & r = f . s )

A17:
[.x2,x1.] c= [.p,g.]
by A5, A6, XXREAL_2:def 12;

A18: [.x2,x1.] c= [.p,g.] by A5, A6, XXREAL_2:def 12;

then f | [.x2,x1.] is continuous by A3, FCONT_1:16;

then consider s being Real such that

A19: s in [.x2,x1.] and

A20: r = f . s by A2, A9, A7, A8, A10, A16, A17, Th15, XBOOLE_1:1;

take s = s; :: thesis: ( s in [.p,g.] & r = f . s )

thus ( s in [.p,g.] & r = f . s ) by A18, A19, A20; :: thesis: verum

end;A18: [.x2,x1.] c= [.p,g.] by A5, A6, XXREAL_2:def 12;

then f | [.x2,x1.] is continuous by A3, FCONT_1:16;

then consider s being Real such that

A19: s in [.x2,x1.] and

A20: r = f . s by A2, A9, A7, A8, A10, A16, A17, Th15, XBOOLE_1:1;

take s = s; :: thesis: ( s in [.p,g.] & r = f . s )

thus ( s in [.p,g.] & r = f . s ) by A18, A19, A20; :: thesis: verum

( s in [.p,g.] & r = f . s ) ; :: thesis: verum