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
f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).]
let f be PartFunc of REAL,REAL; :: thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] )
assume that
A1: p <= g and
A2: [.p,g.] c= dom f and
A3: f | [.p,g.] is continuous ; :: thesis: f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).]
[.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;
now :: thesis: for y being Element of REAL holds
( ( y in f .: [.p,g.] implies y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] ) & ( y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] implies y in f .: [.p,g.] ) )
let y be Element of REAL ; :: thesis: ( ( y in f .: [.p,g.] implies y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] ) & ( y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] implies y in f .: [.p,g.] ) )
thus ( y in f .: [.p,g.] implies y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] ) :: thesis: ( y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] implies y in f .: [.p,g.] )
proof
assume A5: y in f .: [.p,g.] ; :: thesis: y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).]
then A6: y >= lower_bound (f .: [.p,g.]) by A4, SEQ_4:def 2;
y <= upper_bound (f .: [.p,g.]) by A4, A5, SEQ_4:def 1;
then y in { s where s is Real : ( lower_bound (f .: [.p,g.]) <= s & s <= upper_bound (f .: [.p,g.]) ) } by A6;
hence y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] by RCOMP_1:def 1; :: thesis: verum
end;
assume y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] ; :: thesis: y in f .: [.p,g.]
then ex x0 being Real st
( x0 in [.p,g.] & y = f . x0 ) by A1, A2, A3, Th16;
hence y in f .: [.p,g.] by A2, FUNCT_1:def 6; :: thesis: verum
end;
hence f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] by SUBSET_1:3; :: thesis: verum