let n, m be non zero 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 holds
( f is_differentiable_in x iff g is_differentiable_in 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 holds
( f is_differentiable_in x iff g is_differentiable_in 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 holds
( f is_differentiable_in x iff g is_differentiable_in y )
let x be Element of REAL m; :: thesis: for y being Point of (REAL-NS m) st f = g & x = y holds
( f is_differentiable_in x iff g is_differentiable_in y )
let y be Point of (REAL-NS m); :: thesis: ( f = g & x = y implies ( f is_differentiable_in x iff g is_differentiable_in y ) )
assume A1: ( f = g & x = y ) ; :: thesis: ( f is_differentiable_in x iff g is_differentiable_in y )

hereby :: thesis: ( g is_differentiable_in y implies f is_differentiable_in x )

assume f is_differentiable_in x ; :: thesis: g is_differentiable_in 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 & g is_differentiable_in y ) by PDIFF_1:def 7;
hence g is_differentiable_in y by A1; :: thesis: verum

end;

assume g is_differentiable_in y ; :: thesis: f is_differentiable_in x
hence f is_differentiable_in x by A1, PDIFF_1:def 7; :: thesis: verum