theorem LMX1: :: NDIFF_7:51

for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for f being PartFunc of [:X,Y:],W st f is_differentiable_on Z holds
( f `| Z is_continuous_on Z iff (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z )