theorem :: PDIFF_9:56

for m being non zero Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1) st <>* f = g & X c= dom f & f is_differentiable_on X holds
( g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (proj (1,1)) * ((g `| X) /. x) ) )