:: deftheorem Def5 defines diff FDIFF_1:def 5 :
for f being PartFunc of REAL,REAL
for x0 being Real st f is_differentiable_in x0 holds
for b₃ being Real holds
( b₃ = diff (f,x0) iff ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc ex R being RestFunc st
( b₃ = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );