let m be non zero Element of NAT ; :: thesis:
let X be Subset of (REAL m); :: thesis:
let f be PartFunc of (REAL m),REAL; :: thesis:
let g be PartFunc of (REAL m),(REAL 1); :: thesis:
let i be Nat; :: thesis:
assume A1: ( <>* f = g & X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i ) ; :: thesis:
then A2: g is_partial_differentiable_on X,i by Th61;
set ff = f `partial| (X,i);
set gg = g `partial| (X,i);
A3: for x, y being Element of REAL m st x in X & y in X holds
|.(((f `partial| (X,i)) /. x) - ((f `partial| (X,i)) /. y)).| = |.(((g `partial| (X,i)) /. x) - ((g `partial| (X,i)) /. y)).|

proof

let x, y be Element of REAL m; :: thesis:
assume A4: ( x in X & y in X ) ; :: thesis:
then A5: ( (f `partial| (X,i)) /. x = partdiff (f,x,i) & (f `partial| (X,i)) /. y = partdiff (f,y,i) ) by A1, Def6;
A6: ( (g `partial| (X,i)) /. x = partdiff (g,x,i) & (g `partial| (X,i)) /. y = partdiff (g,y,i) ) by A2, A4, PDIFF_7:def 5;
( g is_partial_differentiable_in x,i & g is_partial_differentiable_in y,i ) by A2, A4, A1, PDIFF_7:34;
then ( partdiff (g,x,i) = <*(partdiff (f,x,i))*> & partdiff (g,y,i) = <*(partdiff (f,y,i))*> ) by A1, PDIFF_1:19;
then ((g `partial| (X,i)) /. x) - ((g `partial| (X,i)) /. y) = <*(((f `partial| (X,i)) /. x) - ((f `partial| (X,i)) /. y))*> by A5, A6, RVSUM_1:29;
hence |.(((f `partial| (X,i)) /. x) - ((f `partial| (X,i)) /. y)).| = |.(((g `partial| (X,i)) /. x) - ((g `partial| (X,i)) /. y)).| by Lm1; :: thesis:

end;

A7: dom (g `partial| (X,i)) = X by A2, PDIFF_7:def 5;
A8: dom (f `partial| (X,i)) = X by Def6, A1;

hereby :: thesis:

assume A9: f `partial| (X,i) is_continuous_on X ; :: thesis:

now :: thesis:

let x0 be Element of REAL m; :: thesis:
let r be Real; :: thesis:
assume A10: ( x0 in X & 0 < r ) ; :: thesis:
then consider s being Real such that
A11: ( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r ) ) by A8, A9, Th45;
take s = s; :: thesis:
thus 0 < s by A11; :: thesis:
let x1 be Element of REAL m; :: thesis:
assume A12: ( x1 in X & |.(x1 - x0).| < s ) ; :: thesis:
then |.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r by A11;
hence |.(((g `partial| (X,i)) /. x1) - ((g `partial| (X,i)) /. x0)).| < r by A10, A12, A3; :: thesis:

end;

hence g `partial| (X,i) is_continuous_on X by A7, PDIFF_7:38; :: thesis:

end;

hereby :: thesis:

assume A13: g `partial| (X,i) is_continuous_on X ; :: thesis:

now :: thesis:

let x0 be Element of REAL m; :: thesis:
let r be Real; :: thesis:
assume A14: ( x0 in X & 0 < r ) ; :: thesis:
then consider s being Real such that
A15: ( 0 < s & ( for x1 being Element of REAL m st x1 in X & |.(x1 - x0).| < s holds
|.(((g `partial| (X,i)) /. x1) - ((g `partial| (X,i)) /. x0)).| < r ) ) by A13, PDIFF_7:38;
take s = s; :: thesis:
thus 0 < s by A15; :: thesis:
let x1 be Element of REAL m; :: thesis:
assume A16: ( x1 in X & |.(x1 - x0).| < s ) ; :: thesis:
then |.(((g `partial| (X,i)) /. x1) - ((g `partial| (X,i)) /. x0)).| < r by A15;
hence |.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r by A14, A16, A3; :: thesis:

end;

hence f `partial| (X,i) is_continuous_on X by Th45, A8; :: thesis:

end;