theorem Th8: :: INTEGRA7:8

for X being set
for f, g being PartFunc of REAL,REAL st ( for x being set st x in X holds
g . x <> 0 ) & f is_differentiable_on X & g is_differentiable_on X holds
f / g is_differentiable_on X