let i, j be Element of NAT ; :: thesis: for f being FinSequence st i in dom f & j in dom f & i <= j holds
len (mid (f,i,j)) = (j - i) + 1
let D be FinSequence; :: thesis: ( i in dom D & j in dom D & i <= j implies len (mid (D,i,j)) = (j - i) + 1 )
assume that
A1: i in dom D and
A2: j in dom D and
A3: i <= j ; :: thesis: len (mid (D,i,j)) = (j - i) + 1
j in Seg (len D) by A2, FINSEQ_1:def 3;
then j <= len D by FINSEQ_1:1;
then i <= len D by A3, XXREAL_0:2;
then i -' 1 <= len D by NAT_D:44;
then A4: len (D /^ (i -' 1)) = (len D) - (i -' 1) by RFINSEQ:def 1;
reconsider D1 = D /^ (i -' 1) as FinSequence ;
reconsider k = (j -' i) + 1 as Element of NAT ;
i in Seg (len D) by A1, FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:1;
then j - (i -' 1) = j - (i - 1) by XREAL_1:233;
then A5: j - (i -' 1) = (j - i) + 1 ;
j in Seg (len D) by A2, FINSEQ_1:def 3;
then j <= len D by FINSEQ_1:1;
then j - (i -' 1) <= (len D) - (i -' 1) by XREAL_1:9;
then A6: (j -' i) + 1 <= len (D /^ (i -' 1)) by A3, A4, A5, XREAL_1:233;
mid (D,i,j) = (D /^ (i -' 1)) | ((j -' i) + 1) by A3, FINSEQ_6:def 3
.= D1 | (Seg k) by FINSEQ_1:def 16 ;
then len (mid (D,i,j)) = (j -' i) + 1 by A6, FINSEQ_1:17;
hence len (mid (D,i,j)) = (j - i) + 1 by A3, XREAL_1:233; :: thesis: verum