let D be non empty set ; :: thesis: for f1 being FinSequence of D
for i1, i2, j being 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 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 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, Th117;
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, Th117
.= f1 . ((((i2 -' i1) + 1) + i1) -' 1) by A1, A2, A3, A5, A4, Th117 ;
((i2 -' i1) + 1) + i1 = ((i2 - i1) + 1) + i1 by A2, XREAL_1:233
.= i2 + 1 ;
hence (mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2 by A6, NAT_D:34; :: thesis: verum