theorem :: FCONT_1:47

for g, p being Real
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