let X be set ; :: thesis: for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g holds
( f is_differentiable_on X iff g is_differentiable_on X )
let m, n 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) st f = g holds
( f is_differentiable_on X iff g is_differentiable_on X )
let f be PartFunc of (REAL m),(REAL n); :: thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g holds
( f is_differentiable_on X iff g is_differentiable_on X )
let g be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: ( f = g implies ( f is_differentiable_on X iff g is_differentiable_on X ) )
assume AS: f = g ; :: thesis: ( f is_differentiable_on X iff g is_differentiable_on X )

L: now

assume P0: f is_differentiable_on X ; :: thesis: g is_differentiable_on X
then P1: ( X c= dom f & ( for x being Element of REAL m st x in X holds
f | X is_differentiable_in x ) ) by FDDef1;

now

let y be Point of (REAL-NS m); :: thesis: ( y in X implies g | X is_differentiable_in y )
reconsider x = y as Element of REAL m by REAL_NS1:def 4;
assume y in X ; :: thesis: g | X is_differentiable_in y
then f | X is_differentiable_in x by P0, FDDef1;
then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f | X = g & x = y & g is_differentiable_in y ) by PDIFF_1:def 7;
hence g | X is_differentiable_in y by AS; :: thesis: verum

end;

hence g is_differentiable_on X by AS, P1, NDIFF_1:def 8; :: thesis: verum

end;

now

assume P0: g is_differentiable_on X ; :: thesis: ( X c= dom f & f is_differentiable_on X )
hence X c= dom f by AS, NDIFF_1:def 8; :: thesis: f is_differentiable_on X
P1: ( X c= dom g & ( for x being Point of (REAL-NS m) st x in X holds
g | X is_differentiable_in x ) ) by P0, NDIFF_1:def 8;

now

let y be Element of REAL m; :: thesis: ( y in X implies f | X is_differentiable_in y )
reconsider x = y as Point of (REAL-NS m) by REAL_NS1:def 4;
assume y in X ; :: thesis: f | X is_differentiable_in y
then g | X is_differentiable_in x by P0, NDIFF_1:def 8;
hence f | X is_differentiable_in y by AS, PDIFF_1:def 7; :: thesis: verum

end;

hence f is_differentiable_on X by AS, P1, FDDef1; :: thesis: verum

end;

hence ( f is_differentiable_on X iff g is_differentiable_on X ) by L; :: thesis: verum