let n be non zero Nat; :: thesis: 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; :: 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 that

A1: f = <>* g and

A2: x = y and

A3: f is_partial_differentiable_in x,i ; :: thesis: (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; :: thesis: verum

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; :: 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 that

A1: f = <>* g and

A2: x = y and

A3: f is_partial_differentiable_in x,i ; :: thesis: (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; :: thesis: verum