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:233;
A6: len (f | n) <= n by FINSEQ_5:17;
then n >= i by A3, XXREAL_0:2;
then A7: n - 0 >= i - 1 by XREAL_1:13;
j <= n by A4, A6, XXREAL_0:2;
then j - i <= n - i by XREAL_1:9;
then A8: (j - i) + 1 <= (n - i) + 1 by XREAL_1:6;
i -' 1 = i - 1 by A1, XREAL_1:233;
then A9: n -' (i -' 1) = n - (i - 1) by A7, XREAL_1:233
.= (n - i) + 1 ;
mid ((f | n),i,j) = ((f | n) /^ (i -' 1)) | ((j -' i) + 1) by A2, FINSEQ_6:def 3
.= ((f /^ (i -' 1)) | (n -' (i -' 1))) | ((j -' i) + 1) by FINSEQ_5:80
.= (f /^ (i -' 1)) | ((j -' i) + 1) by A9, A5, A8, FINSEQ_5:77 ;
hence mid (f,i,j) = mid ((f | n),i,j) by A2, FINSEQ_6:def 3; :: thesis: verum