let f be PartFunc of REAL,REAL; :: thesis: for A being Subset of REAL st f is_differentiable_on A holds
( f | A is_differentiable_on A & f `| A = (f | A) `| A )
let A be Subset of REAL; :: thesis: ( f is_differentiable_on A implies ( f | A is_differentiable_on A & f `| A = (f | A) `| A ) )
assume A1: f is_differentiable_on A ; :: thesis: ( f | A is_differentiable_on A & f `| A = (f | A) `| A )
then A c= dom f ;
then A c= (dom f) /\ A by XBOOLE_1:19;
then A2: A c= dom (f | A) by RELAT_1:61;

now :: thesis: for x0 being Real st x0 in A holds
(f | A) | A is_differentiable_in x0

let x0 be Real; :: thesis: ( x0 in A implies (f | A) | A is_differentiable_in x0 )
assume x0 in A ; :: thesis: (f | A) | A is_differentiable_in x0
then f | A is_differentiable_in x0 by A1;
hence (f | A) | A is_differentiable_in x0 by RELAT_1:72; :: thesis: verum

end;

hence A3: f | A is_differentiable_on A by A2; :: thesis: f `| A = (f | A) `| A
then A4: dom ((f | A) `| A) = A by FDIFF_1:def 7;
a5: A is open by A1, FDIFF_1:10;

A5: now :: thesis: for x0 being Element of REAL st x0 in A holds
(f `| A) . x0 = ((f | A) `| A) . x0

let x0 be Element of REAL ; :: thesis: ( x0 in A implies (f `| A) . x0 = ((f | A) `| A) . x0 )
assume A6: x0 in A ; :: thesis: (f `| A) . x0 = ((f | A) `| A) . x0
then consider N2 being Neighbourhood of x0 such that
A7: N2 c= A by a5, RCOMP_1:18;
A8: f | A is_differentiable_in x0 by A1, A6;
A9: f is_differentiable_in x0 by a5, A1, A6, FDIFF_1:9;
then consider N1 being Neighbourhood of x0 such that
A10: N1 c= dom f and
A11: ex L being LinearFunc ex R being RestFunc st
for r being Real st r in N1 holds
(f . r) - (f . x0) = (L . (r - x0)) + (R . (r - x0)) ;
consider L being LinearFunc, R being RestFunc such that
A12: for r being Real st r in N1 holds
(f . r) - (f . x0) = (L . (r - x0)) + (R . (r - x0)) by A11;
consider N being Neighbourhood of x0 such that
A13: N c= N1 and
A14: N c= N2 by RCOMP_1:17;
A15: N c= A by A7, A14;
then A16: N c= dom (f | A) by A2;

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

let r be Real; :: thesis: ( r in N implies ((f | A) . r) - ((f | A) . x0) = (L . (r - x0)) + (R . (r - x0)) )
assume A18: r in N ; :: thesis: ((f | A) . r) - ((f | A) . x0) = (L . (r - x0)) + (R . (r - x0))
then A19: r in A by A15;
thus ((f | A) . r) - ((f | A) . x0) = ((f | A) . r) - (f . x0) by A2, A6, FUNCT_1:47
.= (f . r) - (f . x0) by A2, A19, FUNCT_1:47
.= (L . (r - x0)) + (R . (r - x0)) by A12, A13, A18 ; :: thesis: verum

end;

thus (f `| A) . x0 = diff (f,x0) by A1, A6, FDIFF_1:def 7
.= L . 1 by A9, A10, A12, FDIFF_1:def 5
.= diff ((f | A),x0) by A8, A16, A17, FDIFF_1:def 5
.= ((f | A) `| A) . x0 by A3, A6, FDIFF_1:def 7 ; :: thesis: verum

end;

dom (f `| A) = A by A1, FDIFF_1:def 7;
hence f `| A = (f | A) `| A by A4, A5, PARTFUN1:5; :: thesis: verum