let i be Element of NAT ; :: thesis: for m, n being non empty Element of 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 empty Element of 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 A1: ( F = G & x = y & F is_partial_differentiable_in x,i ) ; :: thesis: (partdiff F,x,i) . <*1*> = partdiff G,y,i
then A2: G is_partial_differentiable_in y,i by Th16;
A3: <*1*> is Element of REAL 1 by FINSEQ_2:118;
( the carrier of (REAL-NS 1) = REAL 1 & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then partdiff F,x,i is Function of (REAL 1),(REAL n) by LOPBAN_1:def 10;
then (partdiff F,x,i) . <*1*> is Element of REAL n by A3, FUNCT_2:7;
hence (partdiff F,x,i) . <*1*> = partdiff G,y,i by A1, A2, Def14; :: thesis: verum