theorem :: FDIFF_12:25

for f1, f2 being PartFunc of REAL,REAL
for I being non empty Interval st I c= dom (f1 / f2) & f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval I holds
( f1 / f2 is_differentiable_on_interval I & (f1 / f2) `\ I = (((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) / (f2 ^2) & ( for x being Real st x in I holds
((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) . x) * (f1 . x))) / ((f2 . x) ^2) ) )