let X be set ; :: thesis: for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds
X is Subset of (REAL m)
let m, n be non empty Element of NAT ; :: thesis: for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds
X is Subset of (REAL m)
let f be PartFunc of (REAL m),(REAL n); :: thesis: ( f is_differentiable_on X implies X is Subset of (REAL m) )
assume f is_differentiable_on X ; :: thesis: X is Subset of (REAL m)
then X c= dom f by Def4;
hence X is Subset of (REAL m) by XBOOLE_1:1; :: thesis: verum