for S, T being RealNormSpace
for f being PartFunc of S,T st dom f is compact & f is_continuous_on dom f holds
rng f is compact