let m, n be non empty Element of NAT ; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: ( 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 ) ) ) :: thesis: ( 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 )

proof

assume A3: f is_differentiable_on Z ; :: thesis: ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) )
hence Z c= dom f by Def4; :: thesis: for x being Element of REAL m st x in Z holds
f is_differentiable_in x
let x be Element of REAL m; :: thesis: ( x in Z implies f is_differentiable_in x )
reconsider y = x as Point of (REAL-NS m) by REAL_NS1:def 4;
assume x in Z ; :: thesis: f is_differentiable_in x
then g is_differentiable_in y by A1, A2, A3, Th30;
hence f is_differentiable_in x by PDIFF_1:def 7; :: thesis: verum

end;

assume A4: ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) ; :: thesis: f is_differentiable_on Z

now

let y be Point of (REAL-NS m); :: thesis: ( y in Z0 implies g is_differentiable_in y )
reconsider x = y as Element of REAL m by REAL_NS1:def 4;
assume y in Z0 ; :: thesis: g is_differentiable_in y
then f is_differentiable_in x by A1, A4;
then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & g is_differentiable_in y ) by PDIFF_1:def 7;
hence g is_differentiable_in y ; :: thesis: verum

end;

hence f is_differentiable_on Z by A1, A2, A4, Th30; :: thesis: verum