let m be non zero 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)
for i being Nat 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)
for i being Nat 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)
for i being Nat 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: for i being Nat 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 Nat; :: 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 A1: ( <>* 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 A2: f is_partial_differentiable_on X,i ; :: thesis: g is_partial_differentiable_on X,i
then A3: X c= dom g by Th3, A1;
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 A2, A1, Th60;
hence g is_partial_differentiable_in x,i by A1, PDIFF_1:18; :: thesis: verum
end;
hence g is_partial_differentiable_on X,i by A3, A1, PDIFF_7:34; :: thesis: verum
end;
hereby :: thesis: verum
assume A4: g is_partial_differentiable_on X,i ; :: thesis: f is_partial_differentiable_on X,i
then A5: X c= dom f by Th3, A1;
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 A4, A1, PDIFF_7:34;
hence f is_partial_differentiable_in x,i by A1, PDIFF_1:18; :: thesis: verum
end;
hence f is_partial_differentiable_on X,i by A1, Th60, A5; :: thesis: verum
end;