let X be set ; :: thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on X holds
X is Subset of COMPLEX
let f be PartFunc of COMPLEX,COMPLEX; :: thesis: ( f is_differentiable_on X implies X is Subset of COMPLEX )
assume f is_differentiable_on X ; :: thesis: X is Subset of COMPLEX
then X c= dom f by Def9;
hence X is Subset of COMPLEX by XBOOLE_1:1; :: thesis: verum