let D be non empty set ; :: thesis: for f, g being FinSequence of D
for i, j being Element of NAT st 1 <= i & i <= j & j <= len f holds
mid ((f ^ g),i,j) = mid (f,i,j)
let f, g be FinSequence of D; :: thesis: for i, j being Element of NAT st 1 <= i & i <= j & j <= len f holds
mid ((f ^ g),i,j) = mid (f,i,j)
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i <= j & j <= len f implies mid ((f ^ g),i,j) = mid (f,i,j) )
assume that
A1: 1 <= i and
A2: i <= j and
A3: j <= len f ; :: thesis: mid ((f ^ g),i,j) = mid (f,i,j)
A4: ((len (f /^ (i -' 1))) + (i - 1)) - (i - 1) = len (f /^ (i -' 1)) ;
len f >= i by A2, A3, XXREAL_0:2;
then (len f) - 0 >= i - 1 by XREAL_1:13;
then A5: len f >= i -' 1 by A1, XREAL_1:233;
(len (f /^ (i -' 1))) + (i -' 1) = ((len f) -' (i -' 1)) + (i -' 1) by RFINSEQ:29
.= len f by A5, XREAL_1:235 ;
then A6: len (f /^ (i -' 1)) = (len f) - (i - 1) by A1, A4, XREAL_1:233
.= ((len f) - i) + 1 ;
(len f) - i >= j - i by A3, XREAL_1:9;
then A7: ((len f) - i) + 1 >= (j - i) + 1 by XREAL_1:6;
j - i >= i - i by A2, XREAL_1:9;
then A8: len (f /^ (i -' 1)) >= (j -' i) + 1 by A7, A6, XREAL_0:def 2;
A9: ( i -' 1 <= i & i <= len f ) by A2, A3, NAT_D:35, XXREAL_0:2;
mid ((f ^ g),i,j) = ((f ^ g) /^ (i -' 1)) | ((j -' i) + 1) by A2, FINSEQ_6:def 3
.= ((f /^ (i -' 1)) ^ g) | ((j -' i) + 1) by A9, GENEALG1:1, XXREAL_0:2
.= (f /^ (i -' 1)) | ((j -' i) + 1) by A8, FINSEQ_5:22 ;
hence mid ((f ^ g),i,j) = mid (f,i,j) by A2, FINSEQ_6:def 3; :: thesis: verum