theorem :: NCFCONT1:80

for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,COMPLEX st dom f is compact & f is_continuous_on dom f holds
rng f is compact