let X be set ; :: thesis: 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
let f, g be PartFunc of REAL,REAL; :: thesis: ( ( for x being set st x in X holds
g . x <> 0 ) & f is_differentiable_on X & g is_differentiable_on X implies f / g is_differentiable_on X )
assume that
A1: for x being set st x in X holds
g . x <> 0 and
A2: f is_differentiable_on X and
A3: g is_differentiable_on X ; :: thesis: f / g is_differentiable_on X
reconsider Z = X as Subset of REAL by A2, FDIFF_1:8;
reconsider Z = Z as open Subset of REAL by A2, FDIFF_1:10;
for x being Real st x in Z holds
g . x <> 0 by A1;
hence f / g is_differentiable_on X by A2, A3, FDIFF_2:21; :: thesis: verum