let p, g be real number ; :: thesis: for f being one-to-one PartFunc of REAL , REAL st p <= g & [.p,g.] c= dom f & ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) holds
((f | [.p,g.]) " ) | (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 increasing or f | [.p,g.] is decreasing ) implies ((f | [.p,g.]) " ) | (f .: [.p,g.]) is continuous )
assume that
A1: ( p <= g & [.p,g.] c= dom f ) and
A2: ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) ; :: thesis: ((f | [.p,g.]) " ) | (f .: [.p,g.]) is continuous
reconsider p = p, g = g as Real by XREAL_0:def 1;

now

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

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

then ((f | [.p,g.]) " ) | (f .: [.p,g.]) is increasing by RFUNCT_2:83;
then A3: ((f | [.p,g.]) " ) | (f .: [.p,g.]) is monotone ;
((f | [.p,g.]) " ) .: (f .: [.p,g.]) = ((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 A1, XBOOLE_1:28 ;
hence ((f | [.p,g.]) " ) | (f .: [.p,g.]) is continuous by A1, A3, Th53; :: thesis: verum

end;

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

then ((f | [.p,g.]) " ) | (f .: [.p,g.]) is decreasing by RFUNCT_2:84;
then A6: ((f | [.p,g.]) " ) | (f .: [.p,g.]) is monotone ;
((f | [.p,g.]) " ) .: (f .: [.p,g.]) = ((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 A1, XBOOLE_1:28 ;
hence ((f | [.p,g.]) " ) | (f .: [.p,g.]) is continuous by A1, A6, Th53; :: thesis: verum

end;

end;

end;

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