theorem :: FDIFF_12:13

for f being PartFunc of REAL,REAL
for x0, r being Real st f is_right_differentiable_in x0 & rng f = {r} holds
Rdiff (f,x0) = 0