theorem Th1: :: CKSPACE1:1
for m being non zero Element of NAT
for Z being set
for I being non empty FinSequence of NAT
for f being PartFunc of (REAL m),REAL st f is_partial_differentiable_on Z,I holds
dom (f `partial| (Z,I)) = Z