theorem Th56: :: NDIFF_5:56

for G being RealNormSpace-Sequence
for S being RealNormSpace
for f being PartFunc of (product G),S
for X being Subset of (product G)
for x being Point of (product G) st X is open & x in X & ( for i being set st i in dom G holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) holds
( f is_differentiable_in x & ( for h being Point of (product G) ex w being FinSequence of S st
( dom w = dom G & ( for i being set st i in dom G holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . h) ) & (diff (f,x)) . h = Sum w ) ) )