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