let m be non empty 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*>;
P0: len <*i*> = 1 by FINSEQ_1:39;
P1: (PartDiffSeq (f,Z,<*i*>)) . 0 = f by TDef5;
1 in Seg 1 ;
then X2: 1 in dom <*i*> by FINSEQ_1:38;
<*i*> /. (0 + 1) = <*i*> . 1 by X2, PARTFUN1:def 6;
then Q1: <*i*> /. (0 + 1) = i by FINSEQ_1:40;

hereby :: thesis: ( f is_partial_differentiable_on Z,i implies f is_partial_differentiable_on Z,<*i*> )

assume PX1: f is_partial_differentiable_on Z,<*i*> ; :: thesis: f is_partial_differentiable_on Z,i
0 <= (len <*i*>) - 1 by P0;
hence f is_partial_differentiable_on Z,i by Q1, P1, PX1, TDef6; :: thesis: verum

end;

assume P3: 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 P5: k = 0 by P0;
then <*i*> /. (k + 1) = <*i*> . 1 by X2, PARTFUN1:def 6;
then <*i*> /. (k + 1) = i by FINSEQ_1:40;
hence (PartDiffSeq (f,Z,<*i*>)) . k is_partial_differentiable_on Z,<*i*> /. (k + 1) by P3, P5, TDef5; :: thesis: verum

end;

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