let n be non zero Element of NAT ; :: thesis:
let Z be open Subset of REAL; :: thesis:
let f be PartFunc of REAL,(REAL n); :: thesis:
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
thus ( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) ) :: thesis:

proof

assume A1: f is_differentiable_on Z ; :: thesis:
A2: Z c= dom g by A1;

now :: thesis:

let x be Real; :: thesis:
assume x in Z ; :: thesis:
then f | Z is_differentiable_in x by A1;
hence g | Z is_differentiable_in x ; :: thesis:

end;

then A3: g is_differentiable_on Z by A2, NDIFF_3:def 5;
for x being Real st x in Z holds
f is_differentiable_in x by A3, NDIFF_3:10;
hence ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) by A1; :: thesis:

end;

assume A4: ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) ; :: thesis:

now :: thesis:

let x be Real; :: thesis:
assume x in Z ; :: thesis:
then f is_differentiable_in x by A4;
hence g is_differentiable_in x ; :: thesis:

end;

then A5: g is_differentiable_on Z by A4, NDIFF_3:10;

now :: thesis:

let x be Real; :: thesis:
assume x in Z ; :: thesis:
then g | Z is_differentiable_in x by A5, NDIFF_3:def 5;
hence f | Z is_differentiable_in x ; :: thesis:

end;

hence f is_differentiable_on Z by A4; :: thesis: