theorem :: FDIFF_4:5

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