let m, n be non empty Element of NAT ; :: thesis:
let X be Subset of (REAL m); :: thesis:
let f be PartFunc of (REAL m),(REAL n); :: thesis:
let r be Real; :: thesis:
assume AS1: f is_differentiable_on X ; :: thesis:
then AS11: X is open by MPDIFF633;
then X c= dom f by AS1, MPDIFF632;
then P3: X c= dom (r (#) f) by VALUED_2:def 39;

let x be Element of REAL m; :: thesis:
assume x in X ; :: thesis:
then f is_differentiable_in x by AS1, AS11, MPDIFF632;
hence r (#) f is_differentiable_in x by PDIFF_6:22; :: thesis:

end;

hence r (#) f is_differentiable_on X by P3, AS11, MPDIFF632; :: thesis:
let x be Element of REAL m; :: thesis:
assume P7: x in X ; :: thesis:
then f is_differentiable_in x by AS1, AS11, MPDIFF632;
then diff ((r (#) f),x) = r (#) (diff (f,x)) by PDIFF_6:22;
hence ((r (#) f) `| X) /. x = r (#) (diff (f,x)) by P3, P7, Def1; :: thesis: