theorem :: CKSPACE1:8

for m being non zero Element of NAT
for Z being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for I, G being non empty FinSequence of NAT st f is_partial_differentiable_on Z,G holds
( f `partial| (Z,(G ^ I)) is_continuous_on Z iff (f `partial| (Z,G)) `partial| (Z,I) is_continuous_on Z ) by Th7;