theorem Th20: :: NDIFF11:20

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