theorem :: NCFCONT2:33

for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS
for Y being Subset of RNS st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds
f .: Y is compact by Th21, NCFCONT1:85;