let i, j, k be 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:25;
A5: 1 + 0 <= i by A2, FINSEQ_3:25;
then i - 1 >= 0 by XREAL_1:19;
then A6: k + 0 <= k + (i - 1) by XREAL_1:6;
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:25;
( i <= len f & 1 <= j ) by A2, A3, FINSEQ_3:25;
then len (mid (f,i,j)) = (j -' i) + 1 by A1, A5, A4, FINSEQ_6:118;
then k <= (j - i) + 1 by A1, A8, XREAL_1:233;
then k <= (j + 1) - i ;
then k + i <= j + 1 by XREAL_1:19;
then ( k + i >= i & (k + i) - 1 <= j ) by NAT_1:11, XREAL_1:20;
then (k + i) -' 1 <= j by A5, XREAL_1:233, XXREAL_0:2;
then A9: (k + i) -' 1 <= len f by A4, XXREAL_0:2;
1 <= k by A7, FINSEQ_3:25;
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:25; :: thesis: verum