let n, m be non zero Nat; 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); 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); 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; 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); ( f = g & x = y & f is_differentiable_in x implies diff (f,x) = diff (g,y) )
assume A1:
( f = g & x = y & f is_differentiable_in x )
; 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 A1; verum