theorem Th24: :: NDIFF_5:24

for G being RealNormSpace-Sequence
for T being RealNormSpace
for i being set
for f being PartFunc of (product G),T
for Z being Subset of (product G) st Z is open holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of (product G) st x in Z holds
f is_partial_differentiable_in x,i ) ) )