let m, n be non empty Element of NAT ; :: thesis: for i being Element of 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 Element of 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 ) ) by Def4;

now

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, Def4;
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 ) by PDIFF_1:def 13;
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, PDIFF_1:def 19; :: 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 ) ) by PDIFF_1:def 19;

now

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, PDIFF_1:def 19;
hence f | Z is_partial_differentiable_in x,i by A1, PDIFF_1:def 13; :: thesis: verum

end;

hence f is_partial_differentiable_on Z,i by A1, A6, Def4; :: thesis: verum