let m be non zero Element of NAT ; :: thesis:
let X be Subset of (REAL m); :: thesis:
let f be PartFunc of (REAL m),REAL; :: thesis:
let r be Real; :: thesis:
assume A1: X c= dom f ; :: thesis:
assume A2: f is_differentiable_on X ; :: thesis:
then A3: X is open by A1, Th55;
A4: X c= dom (r (#) f) by A1, VALUED_1:def 5;

A5: now :: thesis:

let x be Element of REAL m; :: thesis:
assume x in X ; :: thesis:
then f is_differentiable_in x by A2, A3, A1, Th54;
hence ( r (#) f is_differentiable_in x & diff ((r (#) f),x) = r (#) (diff (f,x)) ) by Th52; :: thesis:

end;

then for x being Element of REAL m st x in X holds
r (#) f is_differentiable_in x ;
hence r (#) f is_differentiable_on X by A4, A3, Th54; :: thesis:
let x be Element of REAL m; :: thesis:
assume A6: x in X ; :: thesis:
then ((r (#) f) `| X) /. x = diff ((r (#) f),x) by A4, Def4;
hence ((r (#) f) `| X) /. x = r (#) (diff (f,x)) by A6, A5
.= r (#) ((f `| X) /. x) by A1, A6, Def4 ;
:: thesis: