let D be non empty set ; :: thesis: for f1 being FinSequence of D
for i1, i2, j being Element of NAT st 1 <= i1 & i1 <= i2 & i2 <= len f1 holds
(mid f1,i1,i2) . (len (mid f1,i1,i2)) = f1 . i2
let f1 be FinSequence of D; :: thesis: for i1, i2, j being Element of NAT st 1 <= i1 & i1 <= i2 & i2 <= len f1 holds
(mid f1,i1,i2) . (len (mid f1,i1,i2)) = f1 . i2
let i1, i2, j be Element of NAT ; :: thesis: ( 1 <= i1 & i1 <= i2 & i2 <= len f1 implies (mid f1,i1,i2) . (len (mid f1,i1,i2)) = f1 . i2 )
assume that
A1: 1 <= i1 and
A2: i1 <= i2 and
A3: i2 <= len f1 ; :: thesis: (mid f1,i1,i2) . (len (mid f1,i1,i2)) = f1 . i2
A4: i1 <= len f1 by A2, A3, XXREAL_0:2;
A5: 1 <= i2 by A1, A2, XXREAL_0:2;
then len (mid f1,i1,i2) = (i2 -' i1) + 1 by A1, A2, A3, A4, FINSEQ_6:124;
then 1 <= len (mid f1,i1,i2) by NAT_1:11;
then A6: (mid f1,i1,i2) . (len (mid f1,i1,i2)) = f1 . (((len (mid f1,i1,i2)) + i1) -' 1) by A1, A2, A3, A5, A4, FINSEQ_6:124
.= f1 . ((((i2 -' i1) + 1) + i1) -' 1) by A1, A2, A3, A5, A4, FINSEQ_6:124 ;
((i2 -' i1) + 1) + i1 = ((i2 - i1) + 1) + i1 by A2, XREAL_1:235
.= i2 + 1 ;
hence (mid f1,i1,i2) . (len (mid f1,i1,i2)) = f1 . i2 by A6, NAT_D:34; :: thesis: verum