let f be PartFunc of REAL,REAL; :: thesis: for Z being Subset of REAL
for x0 being Real st Z is open & x0 in Z holds
( ( f is_differentiable_in x0 implies f | Z is_differentiable_in x0 ) & ( f | Z is_differentiable_in x0 implies f is_differentiable_in x0 ) & ( f is_differentiable_in x0 implies diff (f,x0) = diff ((f | Z),x0) ) )
let Z be Subset of REAL; :: thesis: for x0 being Real st Z is open & x0 in Z holds
( ( f is_differentiable_in x0 implies f | Z is_differentiable_in x0 ) & ( f | Z is_differentiable_in x0 implies f is_differentiable_in x0 ) & ( f is_differentiable_in x0 implies diff (f,x0) = diff ((f | Z),x0) ) )
let x0 be Real; :: thesis: ( Z is open & x0 in Z implies ( ( f is_differentiable_in x0 implies f | Z is_differentiable_in x0 ) & ( f | Z is_differentiable_in x0 implies f is_differentiable_in x0 ) & ( f is_differentiable_in x0 implies diff (f,x0) = diff ((f | Z),x0) ) ) )
assume that
AS1: Z is open and
AS3: x0 in Z ; :: thesis: ( ( f is_differentiable_in x0 implies f | Z is_differentiable_in x0 ) & ( f | Z is_differentiable_in x0 implies f is_differentiable_in x0 ) & ( f is_differentiable_in x0 implies diff (f,x0) = diff ((f | Z),x0) ) )
thus ( f is_differentiable_in x0 iff f | Z is_differentiable_in x0 ) :: thesis: ( f is_differentiable_in x0 implies diff (f,x0) = diff ((f | Z),x0) )

proof

thus ( f is_differentiable_in x0 implies f | Z is_differentiable_in x0 ) by LM001, AS1, AS3; :: thesis: ( f | Z is_differentiable_in x0 implies f is_differentiable_in x0 )
thus ( f | Z is_differentiable_in x0 implies f is_differentiable_in x0 ) :: thesis: verum

proof

assume f | Z is_differentiable_in x0 ; :: thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A11: N c= dom (f | Z) and
A12: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by FDIFF_1:def 4;
consider L being LinearFunc, R being RestFunc such that
A17: for x being Real st x in N holds
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A12;
Y0: dom (f | Z) c= dom f by RELAT_1:60;

now :: thesis: for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

let x be Real; :: thesis: ( x in N implies (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A19: x in N ; :: thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
then A20: x in Z by RELAT_1:58, A11, TARSKI:def 3;
((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A17, A19;
then ((f | Z) . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by AS3, FUNCT_1:49;
hence (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A20, FUNCT_1:49; :: thesis: verum

end;

hence f is_differentiable_in x0 by Y0, A11, XBOOLE_1:1, FDIFF_1:def 4; :: thesis: verum

end;

end;

thus ( f is_differentiable_in x0 implies diff (f,x0) = diff ((f | Z),x0) ) by AS1, AS3, LM001; :: thesis: verum