let m, n be non empty Element of NAT ; :: thesis: for i being 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) 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 Element of NAT ; :: thesis: 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) 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); :: thesis: 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) 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); :: thesis: for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m) 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); :: thesis: for Y being Subset of (REAL-NS m) 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); :: thesis: ( 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 AS0: ( 1 <= i & i <= m & X is open & g = f & X = Y & f is_partial_differentiable_on X,i ) ; :: thesis: 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; :: thesis: 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); :: thesis: ( x in X & x = y implies partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*> )
assume AS: ( x in X & x = y ) ; :: thesis: partdiff (f,x,i) = (partdiff (g,y,i)) . <*1*>
then f is_partial_differentiable_in x,i by AS0, 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 AS0, AS; :: thesis: verum