let m, n be non zero Nat; for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open ) holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) )
let f be PartFunc of (REAL m),(REAL n); for Z being Subset of (REAL m) st ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open ) holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) )
let Z be Subset of (REAL m); ( ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open ) implies ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) ) )
assume
ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open )
; ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) )
then consider Z0 being Subset of (REAL-NS m) such that
A1:
( Z = Z0 & Z0 is open )
;
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n )
by REAL_NS1:def 4;
then reconsider g = f as PartFunc of (REAL-NS m),(REAL-NS n) ;
A2:
( g is_differentiable_on Z0 iff ( Z0 c= dom g & ( for x being Point of (REAL-NS m) st x in Z0 holds
g is_differentiable_in x ) ) )
by A1, NDIFF_1:31;
thus
( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) )
by A1, A2, Th30, PDIFF_1:def 7; ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) implies f is_differentiable_on Z )
assume A3:
( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) )
; f is_differentiable_on Z
hence
f is_differentiable_on Z
by A1, A2, A3, Th30; verum