theorem Th14: :: FDIFF_4:14

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