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 & X is open holds
( f is_differentiable_on X iff for x being Element of REAL m st x in X holds
f is_differentiable_in x )
let X be Subset of (REAL m); :: thesis: for f being PartFunc of (REAL m),REAL st X c= dom f & X is open holds
( f is_differentiable_on X iff for x being Element of REAL m st x in X holds
f is_differentiable_in x )
let f be PartFunc of (REAL m),REAL; :: thesis: ( X c= dom f & X is open implies ( f is_differentiable_on X iff for x being Element of REAL m st x in X holds
f is_differentiable_in x ) )
set g = <>* f;
assume A1: X c= dom f ; :: thesis: ( not X is open or ( f is_differentiable_on X iff for x being Element of REAL m st x in X holds
f is_differentiable_in x ) )
assume X is open ; :: thesis: ( f is_differentiable_on X iff for x being Element of REAL m st x in X holds
f is_differentiable_in x )
then A2: ( <>* f is_differentiable_on X iff ( X c= dom (<>* f) & ( for x being Element of REAL m st x in X holds
<>* f is_differentiable_in x ) ) ) by PDIFF_6:32;
thus ( f is_differentiable_on X implies for x being Element of REAL m st x in X holds
f is_differentiable_in x ) by A1, A2, Th53; :: thesis: ( ( for x being Element of REAL m st x in X holds
f is_differentiable_in x ) implies f is_differentiable_on X )
assume for x being Element of REAL m st x in X holds
f is_differentiable_in x ; :: thesis: f is_differentiable_on X
hence f is_differentiable_on X by A1, A2, Th3, Th53, PDIFF_7:def 1; :: thesis: verum