let g, p 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 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 and

A2: [.p,g.] c= dom f and

A3: ( 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 ;

((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 and

A2: [.p,g.] c= dom f and

A3: ( 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 ;

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

hence
((f | [.p,g.]) ") | (f .: [.p,g.]) is continuous
; :: thesis: verumper cases
( f | [.p,g.] is increasing or f | [.p,g.] is decreasing )
by A3;

end;

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

A5: ((f | [.p,g.]) ") .: (f .: [.p,g.]) =
((f | [.p,g.]) ") .: (rng (f | [.p,g.]))
by RELAT_1:115

.= ((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) by FUNCT_1:33

.= rng ((f | [.p,g.]) ") by RELAT_1:113

.= dom (f | [.p,g.]) by FUNCT_1:33

.= (dom f) /\ [.p,g.] by RELAT_1:61

.= [.p,g.] by A2, XBOOLE_1:28 ;

((f | [.p,g.]) ") | (f .: [.p,g.]) is increasing by A4, RFUNCT_2:51;

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

end;.= ((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) by FUNCT_1:33

.= rng ((f | [.p,g.]) ") by RELAT_1:113

.= dom (f | [.p,g.]) by FUNCT_1:33

.= (dom f) /\ [.p,g.] by RELAT_1:61

.= [.p,g.] by A2, XBOOLE_1:28 ;

((f | [.p,g.]) ") | (f .: [.p,g.]) is increasing by A4, RFUNCT_2:51;

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

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

A7: ((f | [.p,g.]) ") .: (f .: [.p,g.]) =
((f | [.p,g.]) ") .: (rng (f | [.p,g.]))
by RELAT_1:115

.= ((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) by FUNCT_1:33

.= rng ((f | [.p,g.]) ") by RELAT_1:113

.= dom (f | [.p,g.]) by FUNCT_1:33

.= (dom f) /\ [.p,g.] by RELAT_1:61

.= [.p,g.] by A2, XBOOLE_1:28 ;

((f | [.p,g.]) ") | (f .: [.p,g.]) is decreasing by A6, RFUNCT_2:52;

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

end;.= ((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) by FUNCT_1:33

.= rng ((f | [.p,g.]) ") by RELAT_1:113

.= dom (f | [.p,g.]) by FUNCT_1:33

.= (dom f) /\ [.p,g.] by RELAT_1:61

.= [.p,g.] by A2, XBOOLE_1:28 ;

((f | [.p,g.]) ") | (f .: [.p,g.]) is decreasing by A6, RFUNCT_2:52;

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