theorem :: FDIFF_4:15

for a being Real
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((- 1) (#) (f ^)) & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) holds
( (- 1) (#) (f ^) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- 1) (#) (f ^)) `| Z) . x = 1 / ((a + x) ^2) ) )