for A being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on A & ( for x0 being Real st x0 in A holds
f . x0 <> 0 ) holds
( f ^ is_differentiable_on A & (f ^) `| A = - ((f `| A) / (f (#) f)) )