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;
now :: thesis: ex s being Real st
( s in [.p,g.] & r = f . s )
per cases ( x1 <= x2 or x2 <= x1 ) ;
suppose A11: x1 <= x2 ; :: thesis: ex s being Real st
( 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;
suppose A16: x2 <= x1 ; :: thesis: ex s being Real st
( 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;
end;
end;
hence ex s being Real st
( s in [.p,g.] & r = f . s ) ; :: thesis: verum