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 & f is_differentiable_in x0 holds
( f | Z is_differentiable_in x0 & 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 & f is_differentiable_in x0 holds
( f | Z is_differentiable_in x0 & diff (f,x0) = diff ((f | Z),x0) )
let x0 be Real; :: thesis: ( Z is open & x0 in Z & f is_differentiable_in x0 implies ( f | Z is_differentiable_in x0 & diff (f,x0) = diff ((f | Z),x0) ) )
assume that
AS1: Z is open and
AS3: x0 in Z and
AS4: f is_differentiable_in x0 ; :: thesis: ( f | Z is_differentiable_in x0 & diff (f,x0) = diff ((f | Z),x0) )
consider N1 being Neighbourhood of x0 such that
A10: N1 c= Z by AS1, AS3, RCOMP_1:18;
consider N being Neighbourhood of x0 such that
A11: N c= dom f and
A12: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by AS4, FDIFF_1:def 4;
consider N2 being Neighbourhood of x0 such that
A13: N2 c= N1 and
A14: N2 c= N by RCOMP_1:17;
A15: N2 c= Z by A10, A13;
N2 c= dom f by A11, A14;
then N2 c= (dom f) /\ Z by A15, XBOOLE_1:19;
then A16: N2 c= dom (f | Z) by RELAT_1:61;
consider L being LinearFunc, R being RestFunc such that
A17: for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A12;
A18: x0 in N2 by RCOMP_1:16;

Y1: 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 A19: 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 A14, A17;
then ((f | Z) . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A16, A19, FUNCT_1:47;
hence ((f | Z) . x) - ((f | Z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A16, A18, FUNCT_1:47; :: thesis: verum

end;

hence f | Z is_differentiable_in x0 by A16, FDIFF_1:def 4; :: thesis: diff (f,x0) = diff ((f | Z),x0)
hence diff ((f | Z),x0) = L . 1 by A16, Y1, FDIFF_1:def 5
.= diff (f,x0) by AS4, A11, A17, FDIFF_1:def 5 ;
:: thesis: verum