let m be non zero Element of NAT ; :: thesis: for f being PartFunc of (REAL m),REAL
for X being non empty Subset of (REAL m)
for d being Real st X is open & f = X --> d holds
( f is_differentiable_on X & dom (f `| X) = X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (REAL m) --> 0 ) )

let f be PartFunc of (REAL m),REAL; :: thesis: for X being non empty Subset of (REAL m)
for d being Real st X is open & f = X --> d holds
( f is_differentiable_on X & dom (f `| X) = X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (REAL m) --> 0 ) )

let X be non empty Subset of (REAL m); :: thesis: for d being Real st X is open & f = X --> d holds
( f is_differentiable_on X & dom (f `| X) = X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (REAL m) --> 0 ) )

let d be Real; :: thesis: ( X is open & f = X --> d implies ( f is_differentiable_on X & dom (f `| X) = X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (REAL m) --> 0 ) ) )

assume A1: ( X is open & f = X --> d ) ; :: thesis: ( f is_differentiable_on X & dom (f `| X) = X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (REAL m) --> 0 ) )

A2: X = dom f by ;
for x being Element of REAL m st x in X holds
f is_differentiable_in x by ;
hence f is_differentiable_on X by ; :: thesis: ( dom (f `| X) = X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (REAL m) --> 0 ) )

thus dom (f `| X) = X by ; :: thesis: for x being Element of REAL m st x in X holds
(f `| X) /. x = (REAL m) --> 0

thus for x being Element of REAL m st x in X holds
(f `| X) /. x = (REAL m) --> 0 :: thesis: verum
proof
let x be Element of REAL m; :: thesis: ( x in X implies (f `| X) /. x = (REAL m) --> 0 )
assume A3: x in X ; :: thesis: (f `| X) /. x = (REAL m) --> 0
thus (f `| X) /. x = diff (f,x) by
.= (REAL m) --> 0 by A3, Th12, A1 ; :: thesis: verum
end;