for f being PartFunc of REAL,REAL
for x0 being Real st f is_differentiable_in x0 holds
( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )