:: deftheorem Def4 defines diff NDIFF_3:def 4 :
for F being RealNormSpace
for f being PartFunc of REAL, the carrier of F
for x0 being Real st f is_differentiable_in x0 holds
for b₄ being Point of F holds
( b₄ = diff (f,x0) iff ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
( b₄ = L /. 1 & ( for x being Real st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) ) ) );