let n, m be non empty Element of NAT ; :: thesis: for i, j being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
let i, j be Element of NAT ; :: thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n)
for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
let f be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for h being PartFunc of (REAL m),(REAL n)
for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
let h be PartFunc of (REAL m),(REAL n); :: thesis: for x being Point of (REAL-NS m)
for z being Element of REAL m st f = h & x = z holds
( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
let x be Point of (REAL-NS m); :: thesis: for z being Element of REAL m st f = h & x = z holds
( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
let z be Element of REAL m; :: thesis: ( f = h & x = z implies ( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j ) )
assume A1: ( f = h & x = z ) ; :: thesis: ( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
then A2: ((Proj j,n) * f) * (reproj i,x) = <>* (((proj j,n) * h) * (reproj i,z)) by Th22;
A3: (Proj i,m) . x = <*((proj i,m) . z)*> by A1, Def4;

hereby :: thesis: ( h is_partial_differentiable_in z,i,j implies f is_partial_differentiable_in x,i,j )

assume f is_partial_differentiable_in x,i,j ; :: thesis: h is_partial_differentiable_in z,i,j
then ((Proj j,n) * f) * (reproj i,x) is_differentiable_in (Proj i,m) . x by Def15;
then ((proj j,n) * h) * (reproj i,z) is_differentiable_in (proj i,m) . z by A2, A3, Th7;
hence h is_partial_differentiable_in z,i,j by Def17; :: thesis: verum

end;

assume h is_partial_differentiable_in z,i,j ; :: thesis: f is_partial_differentiable_in x,i,j
then ((proj j,n) * h) * (reproj i,z) is_differentiable_in (proj i,m) . z by Def17;
then ((Proj j,n) * f) * (reproj i,x) is_differentiable_in (Proj i,m) . x by A2, A3, Th8;
hence f is_partial_differentiable_in x,i,j by Def15; :: thesis: verum