let A be open Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st f is_differentiable_on A holds
( f | A is_differentiable_on A & f `| A = (f | A) `| A )
let f be PartFunc of REAL ,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 A2: ( dom (f `| A) = A & ( for x0 being Real st x0 in A holds
(f `| A) . x0 = diff f,x0 ) ) by FDIFF_1:def 8;
( A c= dom f & ( for x0 being Real st x0 in A holds
f | A is_differentiable_in x0 ) ) by A1, FDIFF_1:def 7;
then A c= (dom f) /\ A by XBOOLE_1:19;
then A3: A c= dom (f | A) by RELAT_1:90;

now

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, FDIFF_1:def 7;
hence (f | A) | A is_differentiable_in x0 by RELAT_1:101; :: thesis: verum

end;

hence A4: f | A is_differentiable_on A by A3, FDIFF_1:def 7; :: thesis: f `| A = (f | A) `| A
then A5: dom ((f | A) `| A) = A by FDIFF_1:def 8;

now

let x0 be 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 A7: f | A is_differentiable_in x0 by A1, FDIFF_1:def 7;
A8: f is_differentiable_in x0 by A1, A6, FDIFF_1:16;
then consider N1 being Neighbourhood of x0 such that
A9: ( N1 c= dom f & ex L being LINEAR ex R being REST st
for r being Real st r in N1 holds
(f . r) - (f . x0) = (L . (r - x0)) + (R . (r - x0)) ) by FDIFF_1:def 5;
consider L being LINEAR, R being REST such that
A10: for r being Real st r in N1 holds
(f . r) - (f . x0) = (L . (r - x0)) + (R . (r - x0)) by A9;
consider N2 being Neighbourhood of x0 such that
A11: N2 c= A by A6, RCOMP_1:39;
consider N being Neighbourhood of x0 such that
A12: ( N c= N1 & N c= N2 ) by RCOMP_1:38;
A13: N c= A by A11, A12, XBOOLE_1:1;
then A14: N c= dom (f | A) by A3, XBOOLE_1:1;

A15: now

let r be Real; :: thesis: ( r in N implies ((f | A) . r) - ((f | A) . x0) = (L . (r - x0)) + (R . (r - x0)) )
assume A16: r in N ; :: thesis: ((f | A) . r) - ((f | A) . x0) = (L . (r - x0)) + (R . (r - x0))
then A17: r in A by A13;
thus ((f | A) . r) - ((f | A) . x0) = ((f | A) . r) - (f . x0) by A3, A6, FUNCT_1:70
.= (f . r) - (f . x0) by A3, A17, FUNCT_1:70
.= (L . (r - x0)) + (R . (r - x0)) by A10, A12, A16 ; :: thesis: verum

end;

thus (f `| A) . x0 = diff f,x0 by A1, A6, FDIFF_1:def 8
.= L . 1 by A8, A9, A10, FDIFF_1:def 6
.= diff (f | A),x0 by A7, A14, A15, FDIFF_1:def 6
.= ((f | A) `| A) . x0 by A4, A6, FDIFF_1:def 8 ; :: thesis: verum

end;

hence f `| A = (f | A) `| A by A2, A5, PARTFUN1:34; :: thesis: verum