let n be non zero Element of NAT ; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n) holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) )

let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,(REAL n) holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) )

let f be PartFunc of REAL,(REAL n); :: thesis: ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) )

reconsider g = f as PartFunc of REAL,() 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: ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) implies f is_differentiable_on Z )
proof
assume A1: f is_differentiable_on Z ; :: thesis: ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) )

A2: Z c= dom g by A1;
now :: thesis: for x being Real st x in Z holds
g | Z is_differentiable_in x
end;
then A3: g is_differentiable_on Z by ;
for x being Real st x in Z holds
f is_differentiable_in x by ;
hence ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) by A1; :: thesis: verum
end;
assume A4: ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) ; :: thesis:
now :: thesis: for x being Real st x in Z holds
g is_differentiable_in x
end;
then A5: g is_differentiable_on Z by ;
now :: thesis: for x being Real st x in Z holds
f | Z is_differentiable_in x
end;
hence f is_differentiable_on Z by A4; :: thesis: verum