let i be Nat; :: thesis: for m, n being non zero Nat

for F being PartFunc of (REAL-NS m),(REAL-NS n)

for G being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds

(partdiff (F,x,i)) . <*1*> = partdiff (G,y,i)

let m, n be non zero Nat; :: thesis: for F being PartFunc of (REAL-NS m),(REAL-NS n)

for G being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for y being Element of REAL m 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 m),(REAL-NS n); :: thesis: for G being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for y being Element of REAL m 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 m),(REAL n); :: thesis: for x being Point of (REAL-NS m)

for y being Element of REAL m 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 m); :: thesis: for y being Element of REAL m 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 m; :: 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: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;

the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;

then partdiff (F,x,i) is Function of (REAL 1),(REAL n) by A4, LOPBAN_1:def 9;

then A5: (partdiff (F,x,i)) . <*jj*> is Element of REAL n by FINSEQ_2:98, FUNCT_2:5;

G is_partial_differentiable_in y,i by A1, A2, A3;

hence (partdiff (F,x,i)) . <*1*> = partdiff (G,y,i) by A1, A2, A5, Def14; :: thesis: verum

for F being PartFunc of (REAL-NS m),(REAL-NS n)

for G being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for y being Element of REAL m st F = G & x = y & F is_partial_differentiable_in x,i holds

(partdiff (F,x,i)) . <*1*> = partdiff (G,y,i)

let m, n be non zero Nat; :: thesis: for F being PartFunc of (REAL-NS m),(REAL-NS n)

for G being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for y being Element of REAL m 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 m),(REAL-NS n); :: thesis: for G being PartFunc of (REAL m),(REAL n)

for x being Point of (REAL-NS m)

for y being Element of REAL m 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 m),(REAL n); :: thesis: for x being Point of (REAL-NS m)

for y being Element of REAL m 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 m); :: thesis: for y being Element of REAL m 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 m; :: 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: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;

the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;

then partdiff (F,x,i) is Function of (REAL 1),(REAL n) by A4, LOPBAN_1:def 9;

then A5: (partdiff (F,x,i)) . <*jj*> is Element of REAL n by FINSEQ_2:98, FUNCT_2:5;

G is_partial_differentiable_in y,i by A1, A2, A3;

hence (partdiff (F,x,i)) . <*1*> = partdiff (G,y,i) by A1, A2, A5, Def14; :: thesis: verum