let m be non empty Element of NAT ; :: thesis: for i being Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1) 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 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) 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) 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) 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: ( <>* 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 AS: ( <>* 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 P1: g is_partial_differentiable_on X,i by CW020;
set ff = f `partial| (X,i);
set gg = g `partial| (X,i);
EQ1: 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 EQ2: ( 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 EQ3: ( (f `partial| (X,i)) /. x = partdiff (f,x,i) & (f `partial| (X,i)) /. y = partdiff (f,y,i) ) by AS, DefPDX;
EQ5: ( (g `partial| (X,i)) /. x = partdiff (g,x,i) & (g `partial| (X,i)) /. y = partdiff (g,y,i) ) by P1, EQ2, PDIFF_7:def 5;
( g is_partial_differentiable_in x,i & g is_partial_differentiable_in y,i ) by P1, EQ2, AS, PDIFF_7:34;
then ( partdiff (g,x,i) = <*(partdiff (f,x,i))*> & partdiff (g,y,i) = <*(partdiff (f,y,i))*> ) by AS, 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 EQ3, EQ5, 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 XTh30D; :: thesis: verum

end;

D1: dom (g `partial| (X,i)) = X by P1, PDIFF_7:def 5;
D2: dom (f `partial| (X,i)) = X by DefPDX, AS;

hereby :: thesis: ( g `partial| (X,i) is_continuous_on X implies f `partial| (X,i) is_continuous_on X )

assume Q2: 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 Q40: ( 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
Q41: ( 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 D2, Q2, XTh38;
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 Q41; :: 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 Q42: ( 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 Q41;
hence |.(((g `partial| (X,i)) /. x1) - ((g `partial| (X,i)) /. x0)).| < r by Q40, Q42, EQ1; :: thesis: verum

end;

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

end;

hereby :: thesis: verum

assume Q2: 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 Q40: ( 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
Q41: ( 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 Q2, 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 Q41; :: 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 Q42: ( 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 Q41;
hence |.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r by Q40, Q42, EQ1; :: thesis: verum

end;

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

end;