let m be non zero Element of NAT ; :: thesis: for X being Subset of (REAL m)
for I being non empty FinSequence of NAT
for f being PartFunc of (REAL m),REAL st f is_partial_differentiable_on X,I holds
dom (f `partial| (X,I)) = X
let Z be Subset of (REAL m); :: thesis: for I being non empty FinSequence of NAT
for f being PartFunc of (REAL m),REAL st f is_partial_differentiable_on Z,I holds
dom (f `partial| (Z,I)) = Z
let I be non empty FinSequence of NAT ; :: thesis: for f being PartFunc of (REAL m),REAL st f is_partial_differentiable_on Z,I holds
dom (f `partial| (Z,I)) = Z
let f be PartFunc of (REAL m),REAL; :: thesis: ( f is_partial_differentiable_on Z,I implies dom (f `partial| (Z,I)) = Z )
reconsider k = (len I) - 1 as Element of NAT by INT_1:5, FINSEQ_1:20;
assume f is_partial_differentiable_on Z,I ; :: thesis: dom (f `partial| (Z,I)) = Z
then A1: (PartDiffSeq (f,Z,I)) . k is_partial_differentiable_on Z,I /. (k + 1) ;
dom ((PartDiffSeq (f,Z,I)) . (k + 1)) = dom (((PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1)))) by PDIFF_9:def 7;
hence dom (f `partial| (Z,I)) = Z by A1, PDIFF_9:def 6; :: thesis: verum