let X be set ; :: thesis: for n being non zero 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 zero 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 ) ) ;

A3: Z c= dom f by A1, A2;

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

then A4: g is_differentiable_on Z by A1, NDIFF_3:24;

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 zero 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 ) ) ;

A3: Z c= dom f by A1, A2;

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

then
g is_differentiable_on X
by A2, NDIFF_3:def 5;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;

hence g | X is_differentiable_in x ; :: thesis: verum

end;assume x in X ; :: thesis: g | X is_differentiable_in x

then f | X is_differentiable_in x by A1;

hence g | X is_differentiable_in x ; :: thesis: verum

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

hence
f is_differentiable_on Z
by A3; :: thesis: verumf | 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 ; :: thesis: verum

end;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 ; :: thesis: verum