for m being non zero Element of NAT
for I being non empty FinSequence of NAT
for X being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for d being Real st X is open & f = X --> d & rng I c= Seg m holds
( (PartDiffSeq (f,X,I)) . 0 = X --> d & ( for i being Element of NAT st 1 <= i & i <= len I holds
(PartDiffSeq (f,X,I)) . i = X --> 0 ) )