theorem :: FDIFF_8:4

for a, b 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 = x + a & f2 . x = x - b ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = ((- a) - b) / ((x - b) ^2) ) )