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 & f is_partial_differentiable_in x,i,j holds
(partdiff f,x,i,j) . <*1*> = <*(partdiff h,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 & f is_partial_differentiable_in x,i,j holds
(partdiff f,x,i,j) . <*1*> = <*(partdiff h,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 & f is_partial_differentiable_in x,i,j holds
(partdiff f,x,i,j) . <*1*> = <*(partdiff h,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 & f is_partial_differentiable_in x,i,j holds
(partdiff f,x,i,j) . <*1*> = <*(partdiff h,z,i,j)*>
let x be Point of (REAL-NS m); :: thesis: for z being Element of REAL m st f = h & x = z & f is_partial_differentiable_in x,i,j holds
(partdiff f,x,i,j) . <*1*> = <*(partdiff h,z,i,j)*>
let z be Element of REAL m; :: thesis: ( f = h & x = z & f is_partial_differentiable_in x,i,j implies (partdiff f,x,i,j) . <*1*> = <*(partdiff h,z,i,j)*> )
assume that
A1: f = h and
A2: x = z and
A3: f is_partial_differentiable_in x,i,j ; :: thesis: (partdiff f,x,i,j) . <*1*> = <*(partdiff h,z,i,j)*>
A4: (Proj i,m) . x = <*((proj i,m) . z)*> by A2, Def4;
A5: ((Proj j,n) * f) * (reproj i,x) is_differentiable_in (Proj i,m) . x by A3, Def15;
((Proj j,n) * f) * (reproj i,x) = <>* (((proj j,n) * h) * (reproj i,z)) by A1, A2, Th22;
hence (partdiff f,x,i,j) . <*1*> = <*(partdiff h,z,i,j)*> by A4, A5, Th10; :: thesis: verum