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 A c= dom f by FDIFF_1:def 7;
then A c= (dom f) /\ A by XBOOLE_1:19;
then A2: 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 A3: f | A is_differentiable_on A by A2, FDIFF_1:def 7; :: thesis: f `| A = (f | A) `| A
then A4: dom ((f | A) `| A) = A by FDIFF_1:def 8;

A5: 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 consider N2 being Neighbourhood of x0 such that
A7: N2 c= A by RCOMP_1:39;
A8: f | A is_differentiable_in x0 by A1, A6, FDIFF_1:def 7;
A9: f is_differentiable_in x0 by A1, A6, FDIFF_1:16;
then consider N1 being Neighbourhood of x0 such that
A10: N1 c= dom f and
A11: 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
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:38;
A15: N c= A by A7, A14, XBOOLE_1:1;
then A16: N c= dom (f | A) by A2, XBOOLE_1:1;

A17: now

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:70
.= (f . r) - (f . x0) by A2, A19, FUNCT_1:70
.= (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 8
.= L . 1 by A9, A10, A12, FDIFF_1:def 6
.= diff (f | A),x0 by A8, A16, A17, FDIFF_1:def 6
.= ((f | A) `| A) . x0 by A3, A6, FDIFF_1:def 8 ; :: thesis: verum

end;

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