let X be open Subset of REAL; :: thesis: for x0 being Real
for f being PartFunc of REAL,REAL st x0 in X & f is_differentiable_on X holds
diff (f,x0) = diff ((f | X),x0)
let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st x0 in X & f is_differentiable_on X holds
diff (f,x0) = diff ((f | X),x0)
let f be PartFunc of REAL,REAL; :: thesis: ( x0 in X & f is_differentiable_on X implies diff (f,x0) = diff ((f | X),x0) )
assume that
A1: x0 in X and
A2: f is_differentiable_on X ; :: thesis: diff (f,x0) = diff ((f | X),x0)
A3: f | X is_differentiable_in x0 by A1, A2;
then A4: f is_differentiable_in x0 by A1, PDIFFEQ1:2;
consider N being Neighbourhood of x0 such that
A5: ( N c= dom (f | X) & ex L being LinearFunc ex R being RestFunc st
( diff ((f | X),x0) = L . 1 & ( for x being Real st x in N holds
((f | X) . x) - ((f | X) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) by A3, FDIFF_1:def 5;
consider L being LinearFunc, R being RestFunc such that
A6: ( diff ((f | X),x0) = L . 1 & ( for x being Real st x in N holds
((f | X) . x) - ((f | X) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A5;
dom (f | X) c= dom f by RELAT_1:60;
then A7: N c= dom f by A5;
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

proof

let x be Real; :: thesis: ( x in N implies (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A8: x in N ; :: thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
then x in dom (f | X) by A5;
then ( (f | X) . x = f . x & (f | X) . x0 = f . x0 ) by A1, FUNCT_1:49;
hence (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) by A6, A8; :: thesis: verum

end;

hence diff (f,x0) = diff ((f | X),x0) by A6, A4, A7, FDIFF_1:def 5; :: thesis: verum