theorem :: FCONT_1:15
for X being set
for f being PartFunc of REAL,REAL holds
( f | X is continuous iff (f | X) | X is continuous ) ;