let m, n be non zero Nat; :: thesis: for i being Nat
for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st Z is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_partial_differentiable_in x,i ) ) )
let i be Nat; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st Z is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_partial_differentiable_in x,i ) ) )
let f be PartFunc of (REAL m),(REAL n); :: thesis: for Z being Subset of (REAL m) st Z is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_partial_differentiable_in x,i ) ) )
let Z be Subset of (REAL m); :: thesis: ( Z is open & 1 <= i & i <= m implies ( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_partial_differentiable_in x,i ) ) ) )
assume A1: ( Z is open & 1 <= i & i <= m ) ; :: thesis: ( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_partial_differentiable_in x,i ) ) )
then consider Z0 being Subset of (REAL-NS m) such that
A2: ( 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) ;

hereby :: thesis: ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_partial_differentiable_in x,i ) implies f is_partial_differentiable_on Z,i )

assume f is_partial_differentiable_on Z,i ; :: thesis: ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_partial_differentiable_in x,i ) )
then A3: g is_partial_differentiable_on Z0,i by A2, Th33;
hence Z c= dom f by A2; :: thesis: for x being Element of REAL m st x in Z holds
f is_partial_differentiable_in x,i
thus for x being Element of REAL m st x in Z holds
f is_partial_differentiable_in x,i :: thesis: verum

proof

let x be Element of REAL m; :: thesis: ( x in Z implies f is_partial_differentiable_in x,i )
assume A4: x in Z ; :: thesis: f is_partial_differentiable_in x,i
reconsider y = x as Point of (REAL-NS m) by REAL_NS1:def 4;
g is_partial_differentiable_in y,i by A2, A3, A4, A1, Th8;
hence f is_partial_differentiable_in x,i ; :: thesis: verum

end;

end;

assume A5: ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_partial_differentiable_in x,i ) ) ; :: thesis: f is_partial_differentiable_on Z,i

now :: thesis: for y being Point of (REAL-NS m) st y in Z0 holds
g is_partial_differentiable_in y,i

let y be Point of (REAL-NS m); :: thesis: ( y in Z0 implies g is_partial_differentiable_in y,i )
assume A6: y in Z0 ; :: thesis: g is_partial_differentiable_in y,i
reconsider x = y as Element of REAL m by REAL_NS1:def 4;
f is_partial_differentiable_in x,i by A2, A6, A5;
then ex gZ being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = gZ & x = y & gZ is_partial_differentiable_in y,i ) ;
hence g is_partial_differentiable_in y,i ; :: thesis: verum

end;

then g is_partial_differentiable_on Z0,i by A1, Th8, A2, A5;
hence f is_partial_differentiable_on Z,i by Th33, A2; :: thesis: verum