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

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