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 & f is_partial_differentiable_in x,i,j holds

(partdiff (f,x,i,j)) . <*1*> = <*(partdiff (h,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 & 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;

((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

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

((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