let i be Element of NAT ; :: thesis: for m, n being non empty Element of NAT
for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i )
let m, n be non empty Element of NAT ; :: thesis: for F being PartFunc of (REAL-NS m),(REAL-NS n)
for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i )
let F be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for G being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i )
let G be PartFunc of (REAL m),(REAL n); :: thesis: for x being Point of (REAL-NS m)
for y being Element of REAL m st F = G & x = y holds
( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i )
let x be Point of (REAL-NS m); :: thesis: for y being Element of REAL m st F = G & x = y holds
( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i )
let y be Element of REAL m; :: thesis: ( F = G & x = y implies ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i ) )
assume A1: ( F = G & x = y ) ; :: thesis: ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i )

now

assume G is_partial_differentiable_in y,i ; :: thesis: F is_partial_differentiable_in x,i
then ex f1 being PartFunc of (REAL-NS m),(REAL-NS n) ex y1 being Point of (REAL-NS m) st
( G = f1 & y = y1 & f1 is_partial_differentiable_in y1,i ) by Def13;
hence F is_partial_differentiable_in x,i by A1; :: thesis: verum

end;

hence ( F is_partial_differentiable_in x,i iff G is_partial_differentiable_in y,i ) by A1, Def13; :: thesis: verum