theorem :: FCONT_3:19

for p being Real
for f being one-to-one PartFunc of REAL,REAL st ( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) & right_open_halfline p c= dom f holds
((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous