theorem :: FCONT_1:29

for Y being Subset of REAL
for f being PartFunc of REAL,REAL st Y c= dom f & Y is compact & f | Y is continuous holds
f .: Y is compact