let m be non zero Element of NAT ; :: thesis: for i being Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,<*i*> iff f is_partial_differentiable_on Z,i )
let i be Element of NAT ; :: thesis: for Z being set
for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,<*i*> iff f is_partial_differentiable_on Z,i )
let Z be set ; :: thesis: for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,<*i*> iff f is_partial_differentiable_on Z,i )
let f be PartFunc of (REAL m),REAL; :: thesis: ( f is_partial_differentiable_on Z,<*i*> iff f is_partial_differentiable_on Z,i )
set I = <*i*>;
A1: len <*i*> = 1 by FINSEQ_1:39;
A2: (PartDiffSeq (f,Z,<*i*>)) . 0 = f | Z by Def7;
1 in Seg 1 ;
then A3: 1 in dom <*i*> by FINSEQ_1:38;
<*i*> /. (0 + 1) = <*i*> . 1 by A3, PARTFUN1:def 6;
then <*i*> /. (0 + 1) = i ;
hence ( f is_partial_differentiable_on Z,<*i*> implies f is_partial_differentiable_on Z,i ) by A2, A1; :: thesis: ( f is_partial_differentiable_on Z,i implies f is_partial_differentiable_on Z,<*i*> )
assume A4: f is_partial_differentiable_on Z,i ; :: thesis: f is_partial_differentiable_on Z,<*i*>

now :: thesis: for k being Element of NAT st k <= (len <*i*>) - 1 holds
(PartDiffSeq (f,Z,<*i*>)) . k is_partial_differentiable_on Z,<*i*> /. (k + 1)

let k be Element of NAT ; :: thesis: ( k <= (len <*i*>) - 1 implies (PartDiffSeq (f,Z,<*i*>)) . k is_partial_differentiable_on Z,<*i*> /. (k + 1) )
assume k <= (len <*i*>) - 1 ; :: thesis: (PartDiffSeq (f,Z,<*i*>)) . k is_partial_differentiable_on Z,<*i*> /. (k + 1)
then A5: k = 0 by A1;
then <*i*> /. (k + 1) = <*i*> . 1 by A3, PARTFUN1:def 6;
then <*i*> /. (k + 1) = i ;
hence (PartDiffSeq (f,Z,<*i*>)) . k is_partial_differentiable_on Z,<*i*> /. (k + 1) by A4, A5, Def7; :: thesis: verum

end;

hence f is_partial_differentiable_on Z,<*i*> ; :: thesis: verum