theorem :: FCONT_3:17

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