theorem :: NDIFF_5:25

for G being RealNormSpace-Sequence
for F being RealNormSpace
for f being PartFunc of (product G),F
for X, i being set st i in dom G & f is_partial_differentiable_on X,i holds
X is Subset of (product G) by XBOOLE_1:1;