theorem Th15: :: FDIFF_2:15

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