theorem :: FCONT_3:18

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