:: deftheorem defines is_partial_differentiable_in NDIFF_5:def 6 :
for G being RealNormSpace-Sequence
for F being RealNormSpace
for i being set
for f being PartFunc of (product G),F
for x being Element of (product G) holds
( f is_partial_differentiable_in x,i iff f * (reproj ((In (i,(dom G))),x)) is_differentiable_in (proj (In (i,(dom G)))) . x );