let m, n be non zero Element of NAT ; 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 Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) )
let f be 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 Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) )
let g be 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 Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) )
let X be Subset of (REAL m); for Y being Subset of (REAL-NS m) st X = Y & X is open & f = g holds
( ( 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 ) ) iff ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) )
let Y be Subset of (REAL-NS m); ( X = Y & X is open & f = g implies ( ( 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 ) ) iff ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) ) )
assume A1:
( X = Y & X is open & f = g )
; ( ( 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 ) ) iff ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) )
hereby ( g is_differentiable_on Y & g `| Y is_continuous_on Y implies 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 ) )
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 )
;
( g is_differentiable_on Y & g `| Y is_continuous_on Y )now for i being 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
Nat;
( 1 <= i & i <= m implies ( g is_partial_differentiable_on Y,i & g `partial| (Y,i) is_continuous_on Y ) )assume A4:
( 1
<= i &
i <= m )
;
( 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 A3;
hence
(
g is_partial_differentiable_on Y,
i &
g `partial| (
Y,
i)
is_continuous_on Y )
by A1, A4, Th23;
verum end; hence
(
g is_differentiable_on Y &
g `| Y is_continuous_on Y )
by A1, PDIFF_8:22;
verum
end;
assume A5:
( g is_differentiable_on Y & g `| Y is_continuous_on Y )
; 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 )
let i be Nat; ( 1 <= i & i <= m implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )
assume A6:
( 1 <= i & i <= m )
; ( 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, A5, PDIFF_8:22;
hence
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
by A1, A6, Th23; verum