let m, n be non empty Element of NAT ; :: thesis: for X being Subset of (REAL m)
for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds
X is open
let X be Subset of (REAL m); :: thesis: for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds
X is open
let f be PartFunc of (REAL m),(REAL n); :: thesis: ( f is_differentiable_on X implies X is open )
assume f is_differentiable_on X ; :: thesis: X is open
then ex X0 being Subset of (REAL-NS m) st
( X = X0 & X0 is open ) by PDIFF_6:33;
hence X is open by PDIFF_7:def 3; :: thesis: verum