let F be non trivial RealNormSpace; :: thesis: for X being set
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds
X is Subset of REAL
let X be set ; :: thesis: for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds
X is Subset of REAL
let f be PartFunc of REAL, the carrier of F; :: thesis: ( f is_differentiable_on X implies X is Subset of REAL )
assume f is_differentiable_on X ; :: thesis: X is Subset of REAL
then X c= dom f by Def5;
hence X is Subset of REAL by XBOOLE_1:1; :: thesis: verum