let f be PartFunc of REAL,REAL; :: thesis: for Z being Subset of REAL
for x being Real st Z is open & x in Z & Z c= dom f & f is_differentiable_in x holds
diff (f,x) = diff ((f | Z),x)
let Z be Subset of REAL; :: thesis: for x being Real st Z is open & x in Z & Z c= dom f & f is_differentiable_in x holds
diff (f,x) = diff ((f | Z),x)
let x0 be Real; :: thesis: ( Z is open & x0 in Z & Z c= dom f & f is_differentiable_in x0 implies diff (f,x0) = diff ((f | Z),x0) )
assume A1: ( Z is open & x0 in Z & Z c= dom f ) ; :: thesis: ( not f is_differentiable_in x0 or diff (f,x0) = diff ((f | Z),x0) )
assume A2: f is_differentiable_in x0 ; :: thesis: diff (f,x0) = diff ((f | Z),x0)
then A3: f | Z is_differentiable_in x0 by A1, Th14;
consider N1 being Neighbourhood of x0 such that
A4: N1 c= Z by A1, RCOMP_1:18;
consider N being Neighbourhood of x0 such that
A5: N c= dom f and
A6: ex L being LinearFunc ex R being RestFunc st
( diff (f,x0) = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A2, FDIFF_1:def 5;
consider N2 being Neighbourhood of x0 such that
A7: N2 c= N1 and
A8: N2 c= N by RCOMP_1:17;
A9: N2 c= Z by A4, A7;
N2 c= dom f by A5, A8;
then A10: N2 c= (dom f) /\ Z by A9, XBOOLE_1:19;
A11: N2 c= dom (f | Z) by A1, A9, RELAT_1:62;
A12: x0 in N2 by RCOMP_1:16;
consider L being LinearFunc, R being RestFunc such that
A13: ( diff (f,x0) = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A6;

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

let x be Real; :: thesis: ( x in N2 implies ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A14: x in N2 ; :: thesis: ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0))
then (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A8, A13;
then ((f | Z) . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A10, A14, FUNCT_1:48;
hence ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A10, A12, FUNCT_1:48; :: thesis: verum

end;

hence diff ((f | Z),x0) = diff (f,x0) by A3, A11, A13, FDIFF_1:def 5; :: thesis: verum