let i, j, k be Element of NAT ; :: thesis: for D being non empty set
for f being FinSequence of D st i <= j & i in dom f & j in dom f & k in dom (mid f,i,j) holds
(k + i) -' 1 in dom f
let D be non empty set ; :: thesis: for f being FinSequence of D st i <= j & i in dom f & j in dom f & k in dom (mid f,i,j) holds
(k + i) -' 1 in dom f
let f be FinSequence of D; :: thesis: ( i <= j & i in dom f & j in dom f & k in dom (mid f,i,j) implies (k + i) -' 1 in dom f )
assume that
A1: i <= j and
A2: i in dom f and
A3: j in dom f ; :: thesis: ( not k in dom (mid f,i,j) or (k + i) -' 1 in dom f )
A4: j <= len f by A3, FINSEQ_3:27;
A5: 1 + 0 <= i by A2, FINSEQ_3:27;
then i - 1 >= 0 by XREAL_1:21;
then A6: k + 0 <= k + (i - 1) by XREAL_1:8;
assume A7: k in dom (mid f,i,j) ; :: thesis: (k + i) -' 1 in dom f
then A8: k <= len (mid f,i,j) by FINSEQ_3:27;
( i <= len f & 1 <= j ) by A2, A3, FINSEQ_3:27;
then len (mid f,i,j) = (j -' i) + 1 by A1, A5, A4, FINSEQ_6:124;
then k <= (j - i) + 1 by A1, A8, XREAL_1:235;
then k <= (j + 1) - i ;
then k + i <= j + 1 by XREAL_1:21;
then ( k + i >= i & (k + i) - 1 <= j ) by NAT_1:11, XREAL_1:22;
then (k + i) -' 1 <= j by A5, XREAL_1:235, XXREAL_0:2;
then A9: (k + i) -' 1 <= len f by A4, XXREAL_0:2;
1 <= k by A7, FINSEQ_3:27;
then 1 <= (k + i) - 1 by A6, XXREAL_0:2;
then 1 <= (k + i) -' 1 by NAT_D:39;
hence (k + i) -' 1 in dom f by A9, FINSEQ_3:27; :: thesis: verum