let m be non zero Element of NAT ; :: thesis:
let f be PartFunc of (REAL m),REAL; :: thesis:
let X be non empty Subset of (REAL m); :: thesis:
let d be Real; :: thesis:
assume A1: ( X is open & f = X --> d ) ; :: thesis:
A2: X = dom f by A1, FUNCT_2:def 1;
for x being Element of REAL m st x in X holds
f is_differentiable_in x by Th12, A1;
hence f is_differentiable_on X by A2, A1, PDIFF_9:54; :: thesis:
thus dom (f `| X) = X by PDIFF_9:def 4, A2; :: thesis:
thus for x being Element of REAL m st x in X holds
(f `| X) /. x = (REAL m) --> 0 :: thesis:

let x be Element of REAL m; :: thesis:
assume A3: x in X ; :: thesis:
thus (f `| X) /. x = diff (f,x) by A2, PDIFF_9:def 4, A3
.= (REAL m) --> 0 by A3, Th12, A1 ; :: thesis:

end;