for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st dom f is compact & f | (dom f) is continuous holds
rng f is compact