theorem Th3: :: PDIFF_6:3

for n, m being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds
diff (f,x) = diff (g,y)