let f be PartFunc of REAL,REAL; :: thesis: for X being Subset of REAL st X is open & X c= dom f & f is_differentiable_on X holds
(f | X) `| X = f `| X
let X be Subset of REAL; :: thesis: ( X is open & X c= dom f & f is_differentiable_on X implies (f | X) `| X = f `| X )
assume that
AS1: X is open and
AS2: X c= dom f and
AS3: f is_differentiable_on X ; :: thesis: (f | X) `| X = f `| X
A1: f | X is_differentiable_on X by AS1, AS2, AS3, LM003;
A2: ( dom (f `| X) = X & ( for x being Real st x in X holds
(f `| X) . x = diff (f,x) ) ) by FDIFF_1:def 7, AS3;
A3: ( dom ((f | X) `| X) = X & ( for x being Real st x in X holds
((f | X) `| X) . x = diff ((f | X),x) ) ) by FDIFF_1:def 7, A1;

now :: thesis: for x being object st x in dom ((f | X) `| X) holds
((f | X) `| X) . x = (f `| X) . x

let x be object ; :: thesis: ( x in dom ((f | X) `| X) implies ((f | X) `| X) . x = (f `| X) . x )
assume A4: x in dom ((f | X) `| X) ; :: thesis: ((f | X) `| X) . x = (f `| X) . x
then A5: x in X by FDIFF_1:def 7, A1;
reconsider x0 = x as Real by A4;
A6: f is_differentiable_in x0 by AS1, AS3, A5, FDIFF_1:9;
thus ((f | X) `| X) . x = diff ((f | X),x0) by FDIFF_1:def 7, A1, A5
.= diff (f,x0) by A6, AS1, A5, LM002
.= (f `| X) . x by FDIFF_1:def 7, AS3, A5 ; :: thesis: verum

end;

hence (f | X) `| X = f `| X by FUNCT_1:2, A2, A3; :: thesis: verum