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