theorem Th22: :: NDIFF14:22

for S being RealNormSpace-Sequence
for T being RealNormSpace
for Z being Subset of (product S)
for f being PartFunc of (product S),T
for i being set st Z is open & f is_differentiable_on Z holds
( f is_partial_differentiable_on Z,i & ( for x being Point of (product S) st x in Z holds
(f `partial| (Z,i)) /. x = ((f `| Z) /. x) * (reproj ((In (i,(dom S))),(0. (product S)))) ) )