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 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: ( 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 PDIFF_9:def 4, A2; :: 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 A2, PDIFF_9:def 4, A3
.= (REAL m) --> 0 by A3, Th12, A1 ; :: thesis: verum

end;