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