let m be non zero Element of NAT ; :: thesis: for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL st X c= dom f & 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 st X c= dom f & f is_differentiable_on X holds
X is open
let f be PartFunc of (REAL m),REAL; :: thesis: ( X c= dom f & f is_differentiable_on X implies X is open )
reconsider g = <>* f as PartFunc of (REAL m),(REAL 1) ;
assume ( X c= dom f & f is_differentiable_on X ) ; :: thesis: X is open
then g is_differentiable_on X by Th53;
hence X is open by PDIFF_6:33; :: thesis: verum