let m be non zero Element of NAT ; :: thesis: for f being PartFunc of (REAL m),REAL
for Z being Subset of (REAL m)
for i being Element of NAT st Z is open & 1 <= i & i <= m & f is_partial_differentiable_on Z,i holds
f `partial| (Z,<*i*>) = f `partial| (Z,i)
let f be PartFunc of (REAL m),REAL; :: thesis: for Z being Subset of (REAL m)
for i being Element of NAT st Z is open & 1 <= i & i <= m & f is_partial_differentiable_on Z,i holds
f `partial| (Z,<*i*>) = f `partial| (Z,i)
let Z be Subset of (REAL m); :: thesis: for i being Element of NAT st Z is open & 1 <= i & i <= m & f is_partial_differentiable_on Z,i holds
f `partial| (Z,<*i*>) = f `partial| (Z,i)
let i be Element of NAT ; :: thesis: ( Z is open & 1 <= i & i <= m & f is_partial_differentiable_on Z,i implies f `partial| (Z,<*i*>) = f `partial| (Z,i) )
assume A1: ( Z is open & 1 <= i & i <= m & f is_partial_differentiable_on Z,i ) ; :: thesis: f `partial| (Z,<*i*>) = f `partial| (Z,i)
set I = <*i*>;
A2: (PartDiffSeq (f,Z,<*i*>)) . 0 = f | Z by Def7;
1 in Seg 1 ;
then 1 in dom <*i*> by FINSEQ_1:38;
then <*i*> /. (0 + 1) = <*i*> . 1 by PARTFUN1:def 6;
then A3: <*i*> /. (0 + 1) = i ;
thus f `partial| (Z,<*i*>) = (PartDiffSeq (f,Z,<*i*>)) . 1 by FINSEQ_1:39
.= ((PartDiffSeq (f,Z,<*i*>)) . 0) `partial| (Z,(<*i*> /. (0 + 1))) by Def7
.= f `partial| (Z,i) by A2, A3, A1, Th71 ; :: thesis: verum