theorem :: NCFCONT2:31

for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for Y being Subset of CNS1 st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds
f .: Y is compact by Th19, NCFCONT1:83;