:: deftheorem defines is_partial_differentiable_on NDIFF_5:def 8 :
for G being RealNormSpace-Sequence
for F being RealNormSpace
for i being set
for f being PartFunc of (product G),F
for X being set holds
( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Point of (product G) st x in X holds
f | X is_partial_differentiable_in x,i ) ) );