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: ( 1 + 0 <= i & i <= len f ) by A2, FINSEQ_3:27;
A5: ( 1 <= j & j <= len f ) by A3, FINSEQ_3:27;
then A6: len (mid f,i,j) = (j -' i) + 1 by A1, A4, JORDAN3:27;
A7: k + i >= i by NAT_1:11;
assume A8: k in dom (mid f,i,j) ; :: thesis: (k + i) -' 1 in dom f
then k <= len (mid f,i,j) by FINSEQ_3:27;
then k <= (j - i) + 1 by A1, A6, XREAL_1:235;
then k <= (j + 1) - i ;
then k + i <= j + 1 by XREAL_1:21;
then (k + i) - 1 <= j by XREAL_1:22;
then (k + i) -' 1 <= j by A4, A7, XREAL_1:235, XXREAL_0:2;
then A9: (k + i) -' 1 <= len f by A5, XXREAL_0:2;
A10: 1 <= k by A8, FINSEQ_3:27;
i - 1 >= 0 by A4, XREAL_1:21;
then k + 0 <= k + (i - 1) by XREAL_1:8;
then 1 <= (k + i) - 1 by A10, 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