let m, n be non empty 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) st X = Y & X is open & f = g holds
( ( for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & g `| Y 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) st X = Y & X is open & f = g holds
( ( for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & g `| Y 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) st X = Y & X is open & f = g holds
( ( for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & g `| Y is_continuous_on Y ) )
let X be Subset of (REAL m); :: thesis: for Y being Subset of (REAL-NS m) st X = Y & X is open & f = g holds
( ( for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & g `| Y is_continuous_on Y ) )
let Y be Subset of (REAL-NS m); :: thesis: ( X = Y & X is open & f = g implies ( ( for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & g `| Y is_continuous_on Y ) ) )
assume AS0: ( X = Y & X is open & f = g ) ; :: thesis: ( ( for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & g `| Y is_continuous_on Y ) )
then A1: Y is open by OPEN;

hereby :: thesis: ( f is_differentiable_on X & g `| Y is_continuous_on Y implies for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )

assume AS1: for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ; :: thesis: ( f is_differentiable_on X & g `| Y is_continuous_on Y )

now :: thesis: for i being Element of NAT st 1 <= i & i <= m holds
( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y )

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= m implies ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )
assume AS2: ( 1 <= i & i <= m ) ; :: thesis: ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y )
then ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) by AS1;
hence ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) by AS0, AS2, LM1Direct; :: thesis: verum

end;

then ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) by A1, PDIFF_8:22;
hence ( f is_differentiable_on X & g `| Y is_continuous_on Y ) by AS0, PDIFF_6:30; :: thesis: verum

end;

assume ( f is_differentiable_on X & g `| Y is_continuous_on Y ) ; :: thesis: for i being Element of NAT st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
then B2: ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) by AS0, PDIFF_6:30;
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= m implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )
assume AS4: ( 1 <= i & i <= m ) ; :: thesis: ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
then ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) by A1, B2, PDIFF_8:22;
hence ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) by AS0, AS4, LM1Direct; :: thesis: verum