let n be non empty Element of NAT ; :: thesis: for i being Element of NAT
for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of REAL n, REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y holds
( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
let i be Element of NAT ; :: thesis: for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of REAL n, REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n 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 n),(REAL-NS 1); :: thesis: for g being PartFunc of REAL n, REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n 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 n, REAL ; :: thesis: for x being Point of (REAL-NS n)
for y being Element of REAL n 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 n); :: thesis: for y being Element of REAL n 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 n; :: thesis: ( f = <>* g & x = y implies ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i ) )
assume ( f = <>* g & x = y ) ; :: thesis: ( f is_partial_differentiable_in x,i iff g is_partial_differentiable_in y,i )
then A1: ( f * (reproj i,x) = <>* (g * (reproj i,y)) & <*((proj i,n) . y)*> = (Proj i,n) . x ) by Def4, Th13;

hereby :: thesis: ( g is_partial_differentiable_in y,i implies f is_partial_differentiable_in x,i )

assume f is_partial_differentiable_in x,i ; :: thesis: g is_partial_differentiable_in y,i
then f * (reproj i,x) is_differentiable_in (Proj i,n) . x by Def9;
then g * (reproj i,y) is_differentiable_in (proj i,n) . y by A1, Th7;
hence g is_partial_differentiable_in y,i by Def11; :: thesis: verum

end;

assume g is_partial_differentiable_in y,i ; :: thesis: f is_partial_differentiable_in x,i
then g * (reproj i,y) is_differentiable_in (proj i,n) . y by Def11;
then f * (reproj i,x) is_differentiable_in (Proj i,n) . x by A1, Th8;
hence f is_partial_differentiable_in x,i by Def9; :: thesis: verum