let m, n be non zero Nat; :: thesis: for i, j being 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 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 that
A1: f = h and
A2: x = z ; :: thesis: ( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j )
A3: (Proj (i,m)) . x = <*((proj (i,m)) . z)*> by A2, Def4;
((Proj (j,n)) * f) * (reproj (i,x)) = <>* (((proj (j,n)) * h) * (reproj (i,z))) by A1, A2, Th22;
hence ( f is_partial_differentiable_in x,i,j iff h is_partial_differentiable_in z,i,j ) by A3, Th7, Th8; :: thesis: verum