theorem :: FDIFF_5:1

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