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