theorem Th26: :: NDIFF11:26

for m being non zero Nat
for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_differentiable_in x holds
for dx being Element of REAL m ex dy being FinSequence of REAL st
( dom dy = Seg m & ( for i being Nat st 1 <= i & i <= m holds
dy . i = ((proj (i,m)) . dx) * (partdiff (f,x,i)) ) & (diff (f,x)) . dx = Sum dy )