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
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:24;
then A4: f .: [.p,g.] is bounded by A2, A3, FCONT_1:30, RCOMP_1:28;

now

let y be 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 5;
y <= upper_bound (f .: [.p,g.]) by A4, A5, SEQ_4:def 4;
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, Th17;
hence y in f .: [.p,g.] by A2, FUNCT_1:def 12; :: thesis: verum

end;

hence f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] by SUBSET_1:8; :: thesis: verum