theorem :: FDIFF_12:14

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