let m, n be non zero Element of NAT ; for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i holds
for x being Element of REAL m
for y being Point of (REAL-NS m) st x in X & x = y holds
partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*>
let f be PartFunc of (REAL m),(REAL n); for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i holds
for x being Element of REAL m
for y being Point of (REAL-NS m) st x in X & x = y holds
partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*>
let g be PartFunc of (REAL-NS m),(REAL-NS n); for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i holds
for x being Element of REAL m
for y being Point of (REAL-NS m) st x in X & x = y holds
partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*>
let X be Subset of (REAL m); for Y being Subset of (REAL-NS m)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i holds
for x being Element of REAL m
for y being Point of (REAL-NS m) st x in X & x = y holds
partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*>
let Y be Subset of (REAL-NS m); for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i holds
for x being Element of REAL m
for y being Point of (REAL-NS m) st x in X & x = y holds
partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*>
let i be Nat; ( 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i implies for x being Element of REAL m
for y being Point of (REAL-NS m) st x in X & x = y holds
partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*> )
assume A1:
( 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i )
; for x being Element of REAL m
for y being Point of (REAL-NS m) st x in X & x = y holds
partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*>
let x be Element of REAL m; for y being Point of (REAL-NS m) st x in X & x = y holds
partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*>
let y be Point of (REAL-NS m); ( x in X & x = y implies partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*> )
assume A2:
( x in X & x = y )
; partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*>
then
f is_partial_differentiable_in x,i
by A1, PDIFF_7:34;
then
ex g0 being PartFunc of (REAL-NS m),(REAL-NS n) ex y0 being Point of (REAL-NS m) st
( f = g0 & x = y0 & partdiff (f,x,i) = (partdiff (g0,y0,i)) . <*1*> )
by PDIFF_1:def 14;
hence
partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*>
by A1, A2; verum