theorem :: FCONT_3:20

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