let n, m be non empty 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 Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds
diff f,x = diff g,y
let f be PartFunc of (REAL m),(REAL n); :: thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds
diff f,x = diff g,y
let g be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds
diff f,x = diff g,y
let x be Element of REAL m; :: thesis: for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds
diff f,x = diff g,y
let y be Point of (REAL-NS m); :: thesis: ( f = g & x = y & f is_differentiable_in x implies diff f,x = diff g,y )
assume AS: ( f = g & x = y & f is_differentiable_in x ) ; :: thesis: diff f,x = diff g,y
then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & diff f,x = diff g,y ) by PDIFF_1:def 8;
hence diff f,x = diff g,y by AS; :: thesis: verum