let X be set ; :: thesis: for f being PartFunc of REAL,REAL st ( for x being set st x in X holds
f . x <> 0 ) & f is_differentiable_on X holds
f ^ is_differentiable_on X
let f be PartFunc of REAL,REAL; :: thesis: ( ( for x being set st x in X holds
f . x <> 0 ) & f is_differentiable_on X implies f ^ is_differentiable_on X )
assume that
A1: for x being set st x in X holds
f . x <> 0 and
A2: f is_differentiable_on X ; :: thesis: f ^ 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
f . x <> 0 by A1;
hence f ^ is_differentiable_on X by A2, FDIFF_2:22; :: thesis: verum