for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS holds ||.f.|| | X = ||.(f | X).||