let i, j be Element of NAT ; 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; ( 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
; 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 15
;
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; verum