let m, n be non zero Nat; :: thesis: for i being Nat
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for Z being set st f = g holds
( f is_partial_differentiable_on Z,i iff g is_partial_differentiable_on Z,i )
let i be Nat; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for Z being set st f = g holds
( f is_partial_differentiable_on Z,i iff g is_partial_differentiable_on Z,i )
let f be PartFunc of (REAL m),(REAL n); :: thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n)
for Z being set st f = g holds
( f is_partial_differentiable_on Z,i iff g is_partial_differentiable_on Z,i )
let g be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for Z being set st f = g holds
( f is_partial_differentiable_on Z,i iff g is_partial_differentiable_on Z,i )
let Z be set ; :: thesis: ( f = g implies ( f is_partial_differentiable_on Z,i iff g is_partial_differentiable_on Z,i ) )
assume A1: f = g ; :: thesis: ( f is_partial_differentiable_on Z,i iff g is_partial_differentiable_on Z,i )
hereby :: thesis: ( g is_partial_differentiable_on Z,i implies f is_partial_differentiable_on Z,i )
assume A2: f is_partial_differentiable_on Z,i ; :: thesis: g is_partial_differentiable_on Z,i
then A3: ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f | Z is_partial_differentiable_in x,i ) ) ;
now :: thesis: for y being Point of (REAL-NS m) st y in Z holds
g | Z is_partial_differentiable_in y,i
let y be Point of (REAL-NS m); :: thesis: ( y in Z implies g | Z is_partial_differentiable_in y,i )
assume A4: y in Z ; :: thesis: g | Z is_partial_differentiable_in y,i
reconsider x = y as Element of REAL m by REAL_NS1:def 4;
f | Z is_partial_differentiable_in x,i by A2, A4;
then ex gZ being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f | Z = gZ & x = y & gZ is_partial_differentiable_in y,i ) ;
hence g | Z is_partial_differentiable_in y,i by A1; :: thesis: verum
end;
hence g is_partial_differentiable_on Z,i by A1, A3; :: thesis: verum
end;
assume A5: g is_partial_differentiable_on Z,i ; :: thesis: f is_partial_differentiable_on Z,i
then A6: ( Z c= dom g & ( for y being Point of (REAL-NS m) st y in Z holds
g | Z is_partial_differentiable_in y,i ) ) ;
now :: thesis: for x being Element of REAL m st x in Z holds
f | Z is_partial_differentiable_in x,i
let x be Element of REAL m; :: thesis: ( x in Z implies f | Z is_partial_differentiable_in x,i )
assume A7: x in Z ; :: thesis: f | Z is_partial_differentiable_in x,i
reconsider y = x as Point of (REAL-NS m) by REAL_NS1:def 4;
g | Z is_partial_differentiable_in y,i by A5, A7;
hence f | Z is_partial_differentiable_in x,i by A1; :: thesis: verum
end;
hence f is_partial_differentiable_on Z,i by A1, A6; :: thesis: verum