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

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