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

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