for m being non zero Nat
for f being PartFunc of (REAL-NS m),(REAL-NS 1)
for X being Subset of (REAL-NS m)
for x being Point of (REAL-NS m) st X is open & x in X & ( for i being Nat st 1 <= i & i <= m 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 (REAL-NS m) ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w ) ) )