theorem :: PDIFF_6:29

for m, n being non zero Nat
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x0 being Point of (REAL-NS m) holds
( g is_differentiable_in x0 iff for i being Nat st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )