theorem Th1: :: FCONT_1:1

for X being set
for x0 being Real
for f being PartFunc of REAL,REAL st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0