theorem :: NDIFF_7:20

for X, Y being RealNormSpace
for Z being Subset of [:X,Y:] holds IsoCPNrSP (X,Y) is_continuous_on Z by LM015;