let m be non zero Element of NAT ; :: thesis: for Z being set
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 Z be set ; :: 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 )
assume A1: f is_partial_differentiable_on Z,I ; :: thesis: dom (f `partial| (Z,I)) = Z
reconsider k = (len I) - 1 as Element of NAT by INT_1:5, FINSEQ_1:20;
A2: f `partial| (Z,I) = ((PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1))) by PDIFF_9:def 7;
(PartDiffSeq (f,Z,I)) . k is_partial_differentiable_on Z,I /. (k + 1) by A1;
hence dom (f `partial| (Z,I)) = Z by A2, PDIFF_9:def 6; :: thesis: verum