let m, n be non zero Nat; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st f is_differentiable_on Z holds
ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open )
let f be PartFunc of (REAL m),(REAL n); :: thesis: for Z being Subset of (REAL m) st f is_differentiable_on Z holds
ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open )
let Z be Subset of (REAL m); :: thesis: ( f is_differentiable_on Z implies ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 & Z0 is open ) )
assume A1: f is_differentiable_on Z ; :: thesis: ex Z0 being Subset of (REAL-NS m) st
( 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) ;
reconsider Z0 = Z as Subset of (REAL-NS m) by REAL_NS1:def 4;
take Z0 ; :: thesis: ( Z = Z0 & Z0 is open )
g is_differentiable_on Z0 by A1, Th30;
hence ( Z = Z0 & Z0 is open ) by NDIFF_1:32; :: thesis: verum