for S, T being RealNormSpace
for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff (f,x0)) . (x - x0)) + (R /. (x - x0)) ) ) )