let X be set ; :: thesis: for n being non empty Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let n be non empty Element of NAT ; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,(REAL n) st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let f be PartFunc of REAL,(REAL n); :: thesis: ( f is_differentiable_on X & Z c= X implies f is_differentiable_on Z )
assume A1: ( f is_differentiable_on X & Z c= X ) ; :: thesis: f is_differentiable_on Z
then A2: ( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) ) by Def3;
A3: Z c= dom f by A1, A2, XBOOLE_1:1;
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

now :: thesis: for x being Real st x in X holds
g | X is_differentiable_in x

let x be Real; :: thesis: ( x in X implies g | X is_differentiable_in x )
assume x in X ; :: thesis: g | X is_differentiable_in x
then f | X is_differentiable_in x by A1, Def3;
hence g | X is_differentiable_in x by Th2; :: thesis: verum

end;

then g is_differentiable_on X by A2, NDIFF_3:def 5;
then A4: g is_differentiable_on Z by A1, NDIFF_3:24;

now :: thesis: for x being Real st x in Z holds
f | Z is_differentiable_in x

let x be Real; :: thesis: ( x in Z implies f | Z is_differentiable_in x )
assume x in Z ; :: thesis: f | Z is_differentiable_in x
then g | Z is_differentiable_in x by A4, NDIFF_3:def 5;
hence f | Z is_differentiable_in x by Def1; :: thesis: verum

end;

hence f is_differentiable_on Z by A3, Def3; :: thesis: verum