let m be non empty 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 AK: 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 ex Z0 being Subset of (REAL-NS m) st
( Z0 = X & Z0 is open ) by PDIFF_7:def 3;
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;

hereby :: 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 A3: f is_differentiable_on X ; :: thesis: for x being Element of REAL m st x in X holds
f is_differentiable_in x
let x be Element of REAL m; :: thesis: ( x in X implies f is_differentiable_in x )
assume x in X ; :: thesis: f is_differentiable_in x
then <>* f is_differentiable_in x by AK, A2, A3, YTh30;
hence f is_differentiable_in x by PDIFF_7:def 1; :: thesis: verum

end;

assume A4: for x being Element of REAL m st x in X holds
f is_differentiable_in x ; :: thesis: f is_differentiable_on X

now :: thesis: for x being Element of REAL m st x in X holds
<>* f is_differentiable_in x

let x be Element of REAL m; :: thesis: ( x in X implies <>* f is_differentiable_in x )
assume x in X ; :: thesis: <>* f is_differentiable_in x
then f is_differentiable_in x by A4;
hence <>* f is_differentiable_in x by PDIFF_7:def 1; :: thesis: verum

end;

hence f is_differentiable_on X by AK, A2, LMXTh0, YTh30; :: thesis: verum