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