let S be RealNormSpace-Sequence; :: thesis: for T being RealNormSpace
for Z being Subset of (product S)
for k being Element of dom S
for f being PartFunc of (product S),T holds f `partial| (Z,<*k*>) = f `partial| (Z,k)
let T be RealNormSpace; :: thesis: for Z being Subset of (product S)
for k being Element of dom S
for f being PartFunc of (product S),T holds f `partial| (Z,<*k*>) = f `partial| (Z,k)
let Z be Subset of (product S); :: thesis: for k being Element of dom S
for f being PartFunc of (product S),T holds f `partial| (Z,<*k*>) = f `partial| (Z,k)
let k be Element of dom S; :: thesis: for f being PartFunc of (product S),T holds f `partial| (Z,<*k*>) = f `partial| (Z,k)
let f be PartFunc of (product S),T; :: thesis: f `partial| (Z,<*k*>) = f `partial| (Z,k)
set I = <*k*>;
A1: ( len <*k*> = 1 & <*k*> . 1 = k ) by FINSEQ_1:40;
then f `partial| (Z,<*k*>) = (PartDiffSeq (f,Z,<*k*>)) . (len <*k*>) by Def7
.= f `partial| (Z,k) by A1, Def6 ;
hence f `partial| (Z,<*k*>) = f `partial| (Z,k) ; :: thesis: verum