let p, g be Real; :: thesis: for f being one-to-one PartFunc of REAL ,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds
(f " ) | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous
let f be one-to-one PartFunc of REAL ,REAL ; :: thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies (f " ) | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous )
assume that
A1: p <= g and
A2: [.p,g.] c= dom f and
X: f | [.p,g.] is continuous ; :: thesis: (f " ) | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous

now

per cases ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) by A1, Th18, X, A2;

suppose f | [.p,g.] is increasing ; :: thesis: (f " ) | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous

then ((f | [.p,g.]) " ) | (f .: [.p,g.]) is increasing by RFUNCT_2:83;
then ((f " ) | (f .: [.p,g.])) | (f .: [.p,g.]) is increasing by RFUNCT_2:40;
then (f " ) | (f .: [.p,g.]) is increasing by RELAT_1:101;
then (f " ) | (f .: [.p,g.]) is monotone ;
then A3: (f " ) | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is monotone by A1, Th20, X, A2;
(f " ) .: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] = (f " ) .: (f .: [.p,g.]) by A1, Th20, X, A2
.= ((f " ) | (f .: [.p,g.])) .: (f .: [.p,g.]) by RELAT_1:162
.= ((f | [.p,g.]) " ) .: (f .: [.p,g.]) by RFUNCT_2:40
.= ((f | [.p,g.]) " ) .: (rng (f | [.p,g.])) by RELAT_1:148
.= ((f | [.p,g.]) " ) .: (dom ((f | [.p,g.]) " )) by FUNCT_1:55
.= rng ((f | [.p,g.]) " ) by RELAT_1:146
.= dom (f | [.p,g.]) by FUNCT_1:55
.= (dom f) /\ [.p,g.] by RELAT_1:90
.= [.p,g.] by A2, XBOOLE_1:28 ;
hence (f " ) | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous by A1, A3, FCONT_1:53; :: thesis: verum

end;

suppose f | [.p,g.] is decreasing ; :: thesis: (f " ) | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous

then ((f | [.p,g.]) " ) | (f .: [.p,g.]) is decreasing by RFUNCT_2:84;
then ((f " ) | (f .: [.p,g.])) | (f .: [.p,g.]) is decreasing by RFUNCT_2:40;
then (f " ) | (f .: [.p,g.]) is decreasing by RELAT_1:101;
then (f " ) | (f .: [.p,g.]) is monotone ;
then A6: (f " ) | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is monotone by A1, Th20, X, A2;
(f " ) .: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] = (f " ) .: (f .: [.p,g.]) by A1, Th20, X, A2
.= ((f " ) | (f .: [.p,g.])) .: (f .: [.p,g.]) by RELAT_1:162
.= ((f | [.p,g.]) " ) .: (f .: [.p,g.]) by RFUNCT_2:40
.= ((f | [.p,g.]) " ) .: (rng (f | [.p,g.])) by RELAT_1:148
.= ((f | [.p,g.]) " ) .: (dom ((f | [.p,g.]) " )) by FUNCT_1:55
.= rng ((f | [.p,g.]) " ) by RELAT_1:146
.= dom (f | [.p,g.]) by FUNCT_1:55
.= (dom f) /\ [.p,g.] by RELAT_1:90
.= [.p,g.] by A2, XBOOLE_1:28 ;
hence (f " ) | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous by A1, A6, FCONT_1:53; :: thesis: verum

end;

end;

end;

hence (f " ) | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous ; :: thesis: verum