let D be non empty set ; :: thesis: for f being FinSequence of D
for i, j, n being Element of NAT st 1 <= i & i <= j & i <= len (f | n) & j <= len (f | n) holds
mid f,i,j = mid (f | n),i,j
let f be FinSequence of D; :: thesis: for i, j, n being Element of NAT st 1 <= i & i <= j & i <= len (f | n) & j <= len (f | n) holds
mid f,i,j = mid (f | n),i,j
let i, j, n be Element of NAT ; :: thesis: ( 1 <= i & i <= j & i <= len (f | n) & j <= len (f | n) implies mid f,i,j = mid (f | n),i,j )
assume that
A1: 1 <= i and
A2: i <= j and
A3: i <= len (f | n) and
A4: j <= len (f | n) ; :: thesis: mid f,i,j = mid (f | n),i,j
A5: (j -' i) + 1 = (j - i) + 1 by A2, XREAL_1:235;
A6: len (f | n) <= n by FINSEQ_5:19;
then n >= i by A3, XXREAL_0:2;
then A7: n - 0 >= i - 1 by XREAL_1:15;
j <= n by A4, A6, XXREAL_0:2;
then j - i <= n - i by XREAL_1:11;
then A8: (j - i) + 1 <= (n - i) + 1 by XREAL_1:8;
i -' 1 = i - 1 by A1, XREAL_1:235;
then A9: n -' (i -' 1) = n - (i - 1) by A7, XREAL_1:235
.= (n - i) + 1 ;
mid (f | n),i,j = ((f | n) /^ (i -' 1)) | ((j -' i) + 1) by A2, JORDAN3:def 1
.= ((f /^ (i -' 1)) | (n -' (i -' 1))) | ((j -' i) + 1) by JORDAN3:21
.= (f /^ (i -' 1)) | ((j -' i) + 1) by A9, A5, A8, FINSEQ_5:80 ;
hence mid f,i,j = mid (f | n),i,j by A2, JORDAN3:def 1; :: thesis: verum