for X, Y being RealNormSpace
for Z being Subset of (product <*X,Y*>) holds (IsoCPNrSP (X,Y)) " is_continuous_on Z by LM015;