for S being RealNormSpace
for Y being Subset of S
for f being PartFunc of S,S st Y c= dom f & f | Y = id Y holds
f is_continuous_on Y