let m be non zero Element of NAT ; :: thesis: for Z being set
for f being PartFunc of (REAL m),REAL
for I, G being non empty FinSequence of NAT st f is_partial_differentiable_on Z,G holds
(f `partial| (Z,G)) `partial| (Z,I) = f `partial| (Z,(G ^ I))
let Z be set ; :: thesis: for f being PartFunc of (REAL m),REAL
for I, G being non empty FinSequence of NAT st f is_partial_differentiable_on Z,G holds
(f `partial| (Z,G)) `partial| (Z,I) = f `partial| (Z,(G ^ I))
let f be PartFunc of (REAL m),REAL; :: thesis: for I, G being non empty FinSequence of NAT st f is_partial_differentiable_on Z,G holds
(f `partial| (Z,G)) `partial| (Z,I) = f `partial| (Z,(G ^ I))
let I, G be non empty FinSequence of NAT ; :: thesis: ( f is_partial_differentiable_on Z,G implies (f `partial| (Z,G)) `partial| (Z,I) = f `partial| (Z,(G ^ I)) )
assume AS: f is_partial_differentiable_on Z,G ; :: thesis: (f `partial| (Z,G)) `partial| (Z,I) = f `partial| (Z,(G ^ I))
thus (f `partial| (Z,G)) `partial| (Z,I) = (PartDiffSeq (f,Z,(G ^ I))) . ((len G) + (len I)) by Th73, AS
.= f `partial| (Z,(G ^ I)) by FINSEQ_1:22 ; :: thesis: verum