theorem :: NFCONT_2:11

for S, T being RealNormSpace
for f being PartFunc of S,T
for Y being Subset of S st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds
f .: Y is compact by Th7, NFCONT_1:32;