let m, n be non zero Element of NAT ; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )
let f be PartFunc of (REAL m),(REAL n); :: thesis: for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )
let g be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )
let X be Subset of (REAL m); :: thesis: for Y being Subset of (REAL-NS m)
for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )
let Y be Subset of (REAL-NS m); :: thesis: for i being Nat st 1 <= i & i <= m & X is open & g = f & X = Y holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )
let i be Nat; :: thesis: ( 1 <= i & i <= m & X is open & g = f & X = Y implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) ) )
assume A1: ( 1 <= i & i <= m & X is open & g = f & X = Y ) ; :: thesis: ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X iff ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )

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

assume A2: ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ; :: thesis: ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y )
hence g is_partial_differentiable_on Y,i by A1, PDIFF_7:33; :: thesis: g `partial| (Y,i) is_continuous_on Y
then A3: dom (g `partial| (Y,i)) = Y by PDIFF_1:def 20;
for y0 being Point of (REAL-NS m)
for r being Real st y0 in Y & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Y & ||.(y1 - y0).|| < s holds
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r ) )

proof

let y0 be Point of (REAL-NS m); :: thesis: for r being Real st y0 in Y & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Y & ||.(y1 - y0).|| < s holds
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r ) )
let r be Real; :: thesis: ( y0 in Y & 0 < r implies ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Y & ||.(y1 - y0).|| < s holds
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r ) ) )
reconsider x0 = y0 as Element of REAL m by REAL_NS1:def 4;
assume A4: ( y0 in Y & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Y & ||.(y1 - y0).|| < s holds
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r ) )
then consider s being Real such that
A5: ( 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 A1, A2, PDIFF_7:38;
take s ; :: thesis: ( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Y & ||.(y1 - y0).|| < s holds
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r ) )
thus 0 < s by A5; :: thesis: for y1 being Point of (REAL-NS m) st y1 in Y & ||.(y1 - y0).|| < s holds
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r
let y1 be Point of (REAL-NS m); :: thesis: ( y1 in Y & ||.(y1 - y0).|| < s implies ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r )
reconsider x1 = y1 as Element of REAL m by REAL_NS1:def 4;
assume A6: ( y1 in Y & ||.(y1 - y0).|| < s ) ; :: thesis: ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r
then A7: |.(x1 - x0).| < s by REAL_NS1:1, REAL_NS1:5;
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| by A4, A6, A1, A2, Th22;
hence ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r by A7, A5, A6, A1; :: thesis: verum

end;

hence g `partial| (Y,i) is_continuous_on Y by A3, NFCONT_1:19; :: thesis: verum

end;

assume A8: ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) ; :: thesis: ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
then A9: f is_partial_differentiable_on X,i by A1, PDIFF_7:33;
then A10: dom (f `partial| (X,i)) = X by PDIFF_7:def 5;
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 ) )

proof

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 ) ) )
reconsider y0 = x0 as Point of (REAL-NS m) by REAL_NS1:def 4;
assume A11: ( 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
A12: ( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Y & ||.(y1 - y0).|| < s holds
||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r ) ) by A1, A8, NFCONT_1:19;
take 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 A12; :: 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 )
reconsider y1 = x1 as Element of (REAL-NS m) by REAL_NS1:def 4;
assume A13: ( x1 in X & |.(x1 - x0).| < s ) ; :: thesis: |.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r
|.(x1 - x0).| = ||.(y1 - y0).|| by REAL_NS1:1, REAL_NS1:5;
then ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).|| < r by A12, A13, A1;
hence |.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| < r by A11, A13, A1, A9, Th22; :: thesis: verum

end;

hence ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) by A8, A10, A1, PDIFF_7:33, PDIFF_7:38; :: thesis: verum