for Y being Subset of REAL
for f being PartFunc of REAL,REAL st Y c= dom f & Y is compact & f | Y is uniformly_continuous holds
f .: Y is compact by Th9, FCONT_1:29;