let m be non zero Element of NAT ; :: thesis: for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1)
for i being Nat st <>* f = g & X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i holds
( f `partial| (X,i) is_continuous_on X iff g `partial| (X,i) is_continuous_on X )
let X be Subset of (REAL m); :: thesis: for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1)
for i being Nat st <>* f = g & X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i holds
( f `partial| (X,i) is_continuous_on X iff g `partial| (X,i) is_continuous_on X )
let f be PartFunc of (REAL m),REAL; :: thesis: for g being PartFunc of (REAL m),(REAL 1)
for i being Nat st <>* f = g & X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i holds
( f `partial| (X,i) is_continuous_on X iff g `partial| (X,i) is_continuous_on X )
let g be PartFunc of (REAL m),(REAL 1); :: thesis: for i being Nat st <>* f = g & X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i holds
( f `partial| (X,i) is_continuous_on X iff g `partial| (X,i) is_continuous_on X )
let i be Nat; :: thesis: ( <>* f = g & X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i implies ( f `partial| (X,i) is_continuous_on X iff g `partial| (X,i) is_continuous_on X ) )
assume A1: ( <>* f = g & X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i ) ; :: thesis: ( f `partial| (X,i) is_continuous_on X iff g `partial| (X,i) is_continuous_on X )
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: ( x in X & y in X implies |.(((f `partial| (X,i)) /. x) - ((f `partial| (X,i)) /. y)).| = |.(((g `partial| (X,i)) /. x) - ((g `partial| (X,i)) /. y)).| )
assume A4: ( x in X & y in X ) ; :: thesis: |.(((f `partial| (X,i)) /. x) - ((f `partial| (X,i)) /. y)).| = |.(((g `partial| (X,i)) /. x) - ((g `partial| (X,i)) /. y)).|
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: verum

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: ( g `partial| (X,i) is_continuous_on X implies f `partial| (X,i) is_continuous_on X )

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

now :: thesis: for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 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 ) )

let x0 be Element of REAL m; :: thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 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 ) )
let r be Real; :: thesis: ( x0 in X & 0 < r implies ex s being Real st
( 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 ) ) )
assume A10: ( x0 in X & 0 < r ) ; :: thesis: ex s being Real st
( 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 ) )
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: ( 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 ) )
thus 0 < s by A11; :: thesis: 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
let x1 be Element of REAL m; :: thesis: ( x1 in X & |.(x1 - x0).| < s implies |.(((g `partial| (X,i)) /. x1) - ((g `partial| (X,i)) /. x0)).| < r )
assume A12: ( x1 in X & |.(x1 - x0).| < s ) ; :: thesis: |.(((g `partial| (X,i)) /. x1) - ((g `partial| (X,i)) /. x0)).| < r
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: verum

end;

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

end;

hereby :: thesis: verum

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

now :: thesis: for x0 being Element of REAL m
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 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 ) )

let x0 be Element of REAL m; :: thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 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 ) )
let r be Real; :: thesis: ( x0 in X & 0 < r implies ex s being Real st
( 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 ) ) )
assume A14: ( x0 in X & 0 < r ) ; :: thesis: ex s being Real st
( 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 ) )
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: ( 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 ) )
thus 0 < s by A15; :: thesis: 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
let x1 be Element of REAL m; :: thesis: ( x1 in X & |.(x1 - x0).| < s implies |.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r )
assume A16: ( x1 in X & |.(x1 - x0).| < s ) ; :: thesis: |.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r
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: verum

end;

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

end;