let m, n be non zero 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 A1: f is_differentiable_on X ; :: thesis:
then A2: X is open by Th13;
then X c= dom f by A1, Th14;
then A3: 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 A1, A2, Th14;
hence r (#) f is_differentiable_in x by PDIFF_6:22; :: thesis:

end;

hence r (#) f is_differentiable_on X by A3, A2, Th14; :: thesis:
let x be Element of REAL m; :: thesis:
assume A4: x in X ; :: thesis:
then f is_differentiable_in x by A1, A2, Th14;
then diff ((r (#) f),x) = r (#) (diff (f,x)) by PDIFF_6:22;
hence ((r (#) f) `| X) /. x = r (#) (diff (f,x)) by A3, A4, Def1; :: thesis: