let m be non zero Element of NAT ; :: thesis: for Z being set
for f being PartFunc of (REAL m),REAL
for I being non empty FinSequence of NAT st f is_partial_differentiable_on Z,I holds
(f `partial| (Z,I)) | Z = f `partial| (Z,I)
let Z be set ; :: thesis: for f being PartFunc of (REAL m),REAL
for I being non empty FinSequence of NAT st f is_partial_differentiable_on Z,I holds
(f `partial| (Z,I)) | Z = f `partial| (Z,I)
let f be PartFunc of (REAL m),REAL; :: thesis: for I being non empty FinSequence of NAT st f is_partial_differentiable_on Z,I holds
(f `partial| (Z,I)) | Z = f `partial| (Z,I)
let I be non empty FinSequence of NAT ; :: thesis: ( f is_partial_differentiable_on Z,I implies (f `partial| (Z,I)) | Z = f `partial| (Z,I) )
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: (f `partial| (Z,I)) | Z = f `partial| (Z,I)
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 Def7;
then dom ((PartDiffSeq (f,Z,I)) . (k + 1)) = Z by A1, Def6;
hence (f `partial| (Z,I)) | Z = f `partial| (Z,I) by RELAT_1:68; :: thesis: verum