let S be RealNormSpace-Sequence; :: thesis: for T being RealNormSpace
for Z being Subset of (product S)
for I being non empty FinSequence of dom S
for f being PartFunc of (product S),T holds
( PartDiffSeq (f,Z,I,1) = f `partial| (Z,(I . 1)) & ( for i being Nat st 1 <= i & i < len I holds
PartDiffSeq (f,Z,I,(i + 1)) = (PartDiffSeq (f,Z,I,i)) `partial| (Z,(I . (i + 1))) ) )
let T be RealNormSpace; :: thesis: for Z being Subset of (product S)
for I being non empty FinSequence of dom S
for f being PartFunc of (product S),T holds
( PartDiffSeq (f,Z,I,1) = f `partial| (Z,(I . 1)) & ( for i being Nat st 1 <= i & i < len I holds
PartDiffSeq (f,Z,I,(i + 1)) = (PartDiffSeq (f,Z,I,i)) `partial| (Z,(I . (i + 1))) ) )
let Z be Subset of (product S); :: thesis: for I being non empty FinSequence of dom S
for f being PartFunc of (product S),T holds
( PartDiffSeq (f,Z,I,1) = f `partial| (Z,(I . 1)) & ( for i being Nat st 1 <= i & i < len I holds
PartDiffSeq (f,Z,I,(i + 1)) = (PartDiffSeq (f,Z,I,i)) `partial| (Z,(I . (i + 1))) ) )
let I be non empty FinSequence of dom S; :: thesis: for f being PartFunc of (product S),T holds
( PartDiffSeq (f,Z,I,1) = f `partial| (Z,(I . 1)) & ( for i being Nat st 1 <= i & i < len I holds
PartDiffSeq (f,Z,I,(i + 1)) = (PartDiffSeq (f,Z,I,i)) `partial| (Z,(I . (i + 1))) ) )
let f be PartFunc of (product S),T; :: thesis: ( PartDiffSeq (f,Z,I,1) = f `partial| (Z,(I . 1)) & ( for i being Nat st 1 <= i & i < len I holds
PartDiffSeq (f,Z,I,(i + 1)) = (PartDiffSeq (f,Z,I,i)) `partial| (Z,(I . (i + 1))) ) )
1 <= len I by FINSEQ_1:20;
hence PartDiffSeq (f,Z,I,1) = (PartDiffSeq (f,Z,I)) . 1 by Def7
.= f `partial| (Z,(I . 1)) by Def6 ;
:: thesis: for i being Nat st 1 <= i & i < len I holds
PartDiffSeq (f,Z,I,(i + 1)) = (PartDiffSeq (f,Z,I,i)) `partial| (Z,(I . (i + 1)))
let i be Nat; :: thesis: ( 1 <= i & i < len I implies PartDiffSeq (f,Z,I,(i + 1)) = (PartDiffSeq (f,Z,I,i)) `partial| (Z,(I . (i + 1))) )
assume A1: ( 1 <= i & i < len I ) ; :: thesis: PartDiffSeq (f,Z,I,(i + 1)) = (PartDiffSeq (f,Z,I,i)) `partial| (Z,(I . (i + 1)))
then ( 1 <= i + 1 & i + 1 <= len I ) by NAT_1:13;
then A2: PartDiffSeq (f,Z,I,(i + 1)) = (PartDiffSeq (f,Z,I)) . (i + 1) by Def7;
ex g being PartFunc of (product S),(Partdiff_SP (S,T,I,i)) st
( (PartDiffSeq (f,Z,I)) . i = g & (PartDiffSeq (f,Z,I)) . (i + 1) = g `partial| (Z,(I . (i + 1))) ) by Def6, A1;
hence PartDiffSeq (f,Z,I,(i + 1)) = (PartDiffSeq (f,Z,I,i)) `partial| (Z,(I . (i + 1))) by A1, A2, Def7; :: thesis: verum