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 `partial| (Z,<*i*>) = f `partial| (Z,i)
let i be Element of NAT ; :: thesis: for Z being set
for f being PartFunc of (REAL m),REAL holds f `partial| (Z,<*i*>) = f `partial| (Z,i)
let Z be set ; :: thesis: for f being PartFunc of (REAL m),REAL holds f `partial| (Z,<*i*>) = f `partial| (Z,i)
let f be PartFunc of (REAL m),REAL; :: thesis: f `partial| (Z,<*i*>) = f `partial| (Z,i)
set I = <*i*>;
1 in Seg 1 ;
then 1 in dom <*i*> by FINSEQ_1:38;
then <*i*> /. (0 + 1) = <*i*> . 1 by PARTFUN1:def 6;
then Q1: <*i*> /. (0 + 1) = i by FINSEQ_1:40;
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 TDef5
.= f `partial| (Z,i) by Q1, TDef5 ; :: thesis: verum