let m, n be non zero Element of NAT ; :: thesis:
let f be PartFunc of (REAL m),(REAL n); :: thesis:
let g be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis:
let X be Subset of (REAL m); :: thesis:
let Y be Subset of (REAL-NS m); :: thesis:
assume A1: ( X = Y & X is open & f = g ) ; :: thesis:

hereby :: thesis:

assume A3: for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ; :: thesis:

now :: thesis:

let i be Nat; :: thesis:
assume A4: ( 1 <= i & i <= m ) ; :: thesis:
then ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) by A3;
hence ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) by A1, A4, Th23; :: thesis:

end;

hence ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) by A1, PDIFF_8:22; :: thesis:

end;

assume A5: ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) ; :: thesis:
let i be Nat; :: thesis:
assume A6: ( 1 <= i & i <= m ) ; :: thesis:
then ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) by A1, A5, PDIFF_8:22;
hence ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) by A1, A6, Th23; :: thesis: