theorem Th18: :: NDIFF11:18

for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m holds
( f is_differentiable_in x iff for i being Nat st 1 <= i & i <= n holds
ex fi being PartFunc of (REAL m),(REAL 1) st
( fi = (Proj (i,n)) * f & fi is_differentiable_in x ) )