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 A1: ( 1 <= i1 & i1 <= i2 & i2 <= len f1 ) ; :: thesis: (mid f1,i1,i2) . (len (mid f1,i1,i2)) = f1 . i2
then A2: 1 <= i2 by XXREAL_0:2;
A3: i1 <= len f1 by A1, XXREAL_0:2;
then len (mid f1,i1,i2) = (i2 -' i1) + 1 by A1, A2, JORDAN3:27;
then 1 <= len (mid f1,i1,i2) by NAT_1:11;
then A4: (mid f1,i1,i2) . (len (mid f1,i1,i2)) = f1 . (((len (mid f1,i1,i2)) + i1) -' 1) by A1, A2, A3, JORDAN3:27
.= f1 . ((((i2 -' i1) + 1) + i1) -' 1) by A1, A2, A3, JORDAN3:27 ;
((i2 -' i1) + 1) + i1 = ((i2 - i1) + 1) + i1 by A1, XREAL_1:235
.= i2 + 1 ;
hence (mid f1,i1,i2) . (len (mid f1,i1,i2)) = f1 . i2 by A4, NAT_D:34; :: thesis: verum