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:3;
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 2;
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:3;
then j - (i -' 1) = j - (i - 1) by XREAL_1:235;
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:3;
then j - (i -' 1) <= (len D) - (i -' 1) by XREAL_1:11;
then A6: (j -' i) + 1 <= len (D /^ (i -' 1)) by A3, A4, A5, XREAL_1:235;
mid D,i,j = (D /^ (i -' 1)) | ((j -' i) + 1) by A3, JORDAN3:def 1
.= D1 | (Seg k) by FINSEQ_1:def 15 ;
then len (mid D,i,j) = (j -' i) + 1 by A6, FINSEQ_1:21;
hence len (mid D,i,j) = (j - i) + 1 by A3, XREAL_1:235; :: thesis: verum