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 & f is_partial_differentiable_in x,i holds
(partdiff f,x,i) . <*1*> = <*(partdiff g,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 & f is_partial_differentiable_in x,i holds
(partdiff f,x,i) . <*1*> = <*(partdiff g,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 & f is_partial_differentiable_in x,i holds
(partdiff f,x,i) . <*1*> = <*(partdiff g,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 & f is_partial_differentiable_in x,i holds
(partdiff f,x,i) . <*1*> = <*(partdiff g,y,i)*>
let x be Point of (REAL-NS n); :: thesis: for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds
(partdiff f,x,i) . <*1*> = <*(partdiff g,y,i)*>
let y be Element of REAL n; :: thesis: ( f = <>* g & x = y & f is_partial_differentiable_in x,i implies (partdiff f,x,i) . <*1*> = <*(partdiff g,y,i)*> )
assume ( f = <>* g & x = y & f is_partial_differentiable_in x,i ) ; :: thesis: (partdiff f,x,i) . <*1*> = <*(partdiff g,y,i)*>
then ( f * (reproj i,x) = <>* (g * (reproj i,y)) & f * (reproj i,x) is_differentiable_in (Proj i,n) . x & <*((proj i,n) . y)*> = (Proj i,n) . x ) by Def4, Def9, Th13;
hence (partdiff f,x,i) . <*1*> = <*(partdiff g,y,i)*> by Th10; :: thesis: verum