for S being RealNormSpace
for f being PartFunc of S,S st f = id (dom f) holds
f is_continuous_on dom f