for m being non zero Nat
for f being PartFunc of (REAL m),(REAL 1)
for X being Subset of (REAL m)
for x being Element of REAL 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 Element of REAL 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 = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & (diff (f,x)) . h = Sum w ) ) )