let n be non zero Nat; for i being 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 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 f be 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 g be 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 x be 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 y be Element of REAL n; ( f = <>* g & x = y & f is_partial_differentiable_in x,i implies (partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*> )
assume that
A1:
f = <>* g
and
A2:
x = y
and
A3:
f is_partial_differentiable_in x,i
; (partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*>
A4:
f * (reproj (i,x)) is_differentiable_in (Proj (i,n)) . x
by A3;
A5:
<*((proj (i,n)) . y)*> = (Proj (i,n)) . x
by A2, Def4;
f * (reproj (i,x)) = <>* (g * (reproj (i,y)))
by A1, A2, Th13;
hence
(partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*>
by A4, A5, Th10; verum