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