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,(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: ( Z c= dom f & ( for x being Real st x in Z holds

f is_differentiable_in x ) implies f is_differentiable_on Z )

f is_differentiable_in x ) ) ; :: thesis: f is_differentiable_on Z

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,(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: ( 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 A4:
( Z c= dom f & ( for x being Real st x in Z holds
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;

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: verum

end;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

then A3:
g is_differentiable_on Z
by A2, NDIFF_3:def 5;g | Z is_differentiable_in x

let x be Real; :: thesis: ( x in Z implies g | Z is_differentiable_in x )

assume x in Z ; :: thesis: g | Z is_differentiable_in x

then f | Z is_differentiable_in x by A1;

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

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

then f | Z is_differentiable_in x by A1;

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

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: verum

f is_differentiable_in x ) ) ; :: thesis: f is_differentiable_on Z

now :: thesis: for x being Real st x in Z holds

g is_differentiable_in x

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

let x be Real; :: thesis: ( x in Z implies g is_differentiable_in x )

assume x in Z ; :: thesis: g is_differentiable_in x

then f is_differentiable_in x by A4;

hence g is_differentiable_in x ; :: thesis: verum

end;assume x in Z ; :: thesis: g is_differentiable_in x

then f is_differentiable_in x by A4;

hence g is_differentiable_in x ; :: thesis: verum

now :: thesis: for x being Real st x in Z holds

f | Z is_differentiable_in x

hence
f is_differentiable_on Z
by A4; :: 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 A5, 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 A5, NDIFF_3:def 5;

hence f | Z is_differentiable_in x ; :: thesis: verum