let X be set ; :: thesis: for m, n being non zero 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 zero 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 A1: f = g ; :: thesis: ( f is_differentiable_on X iff g is_differentiable_on X )

A2: now :: thesis: ( f is_differentiable_on X implies g is_differentiable_on X )

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

now :: thesis: for y being Point of (REAL-NS m) st y in X holds
g | X is_differentiable_in y

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 A3;
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 A1; :: thesis: verum

end;

hence g is_differentiable_on X by A1, A4, NDIFF_1:def 8; :: thesis: verum

end;

now :: thesis: ( g is_differentiable_on X implies ( X c= dom f & f is_differentiable_on X ) )

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

now :: thesis: for y being Element of REAL m st y in X holds
f | X is_differentiable_in y

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 A5, NDIFF_1:def 8;
hence f | X is_differentiable_in y by A1, PDIFF_1:def 7; :: thesis: verum

end;

hence f is_differentiable_on X by A1, A6; :: thesis: verum

end;

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