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 holds
( f is_partial_differentiable_on X,i iff g is_partial_differentiable_on X,i )
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 holds
( f is_partial_differentiable_on X,i iff g is_partial_differentiable_on X,i )
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 holds
( f is_partial_differentiable_on X,i iff g is_partial_differentiable_on X,i )
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 holds
( f is_partial_differentiable_on X,i iff g is_partial_differentiable_on X,i )
let g be PartFunc of (REAL m),(REAL 1); :: thesis: ( <>* f = g & X is open & 1 <= i & i <= m implies ( f is_partial_differentiable_on X,i iff g is_partial_differentiable_on X,i ) )
assume AS: ( <>* f = g & X is open & 1 <= i & i <= m ) ; :: thesis: ( f is_partial_differentiable_on X,i iff g is_partial_differentiable_on X,i )

hereby :: thesis: ( g is_partial_differentiable_on X,i implies f is_partial_differentiable_on X,i )

assume P2: f is_partial_differentiable_on X,i ; :: thesis: g is_partial_differentiable_on X,i
then X c= dom f by AS, PDIFF734;
then P3: X c= dom g by LMXTh0, AS;

now :: thesis: for x being Element of REAL m st x in X holds
g is_partial_differentiable_in x,i

let x be Element of REAL m; :: thesis: ( x in X implies g is_partial_differentiable_in x,i )
assume x in X ; :: thesis: g is_partial_differentiable_in x,i
then f is_partial_differentiable_in x,i by P2, AS, PDIFF734;
hence g is_partial_differentiable_in x,i by AS, PDIFF_1:18; :: thesis: verum

end;

hence g is_partial_differentiable_on X,i by P3, AS, PDIFF_7:34; :: thesis: verum

end;

hereby :: thesis: verum

assume P3: g is_partial_differentiable_on X,i ; :: thesis: f is_partial_differentiable_on X,i
then X c= dom g by AS, PDIFF_7:34;
then P4: X c= dom f by LMXTh0, AS;

now :: thesis: for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i

let x be Element of REAL m; :: thesis: ( x in X implies f is_partial_differentiable_in x,i )
assume x in X ; :: thesis: f is_partial_differentiable_in x,i
then g is_partial_differentiable_in x,i by P3, AS, PDIFF_7:34;
hence f is_partial_differentiable_in x,i by AS, PDIFF_1:18; :: thesis: verum

end;

hence f is_partial_differentiable_on X,i by AS, PDIFF734, P4; :: thesis: verum

end;