theorem :: FDIFF_3:14

for f being PartFunc of REAL,REAL
for x0 being Real st f is_left_differentiable_in x0 & f . x0 <> 0 holds
( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )