let D be non empty set ; :: thesis: for f1 being FinSequence of D
for i1, i2, j being Nat st 1 <= i1 & i1 <= len f1 & 1 <= 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 <= len f1 & 1 <= 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 <= len f1 & 1 <= i2 & i2 <= len f1 implies (mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2 )
assume that
A1: 1 <= i1 and
A2: i1 <= len f1 and
A3: 1 <= i2 and
A4: i2 <= len f1 ; :: thesis: (mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2

per cases ( i1 <= i2 or i1 > i2 ) ;

suppose i1 <= i2 ; :: thesis: (mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2

hence (mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2 by A1, A4, Th10; :: thesis: verum

end;

suppose A5: i1 > i2 ; :: thesis: (mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2

0 <= i2 - 1 by A3, XREAL_1:48;
then i1 - 0 >= i1 - (i2 - 1) by XREAL_1:10;
then i1 >= (i1 - i2) + 1 ;
then (i1 -' i2) + 1 <= i1 by A5, XREAL_1:233;
then A6: (i1 -' ((i1 -' i2) + 1)) + 1 = (i1 - ((i1 -' i2) + 1)) + 1 by XREAL_1:233
.= i1 - (i1 -' i2)
.= i1 - (i1 - i2) by A5, XREAL_1:233
.= i2 ;
len (mid (f1,i1,i2)) = (i1 -' i2) + 1 by A1, A2, A3, A4, A5, Th117;
then 1 <= len (mid (f1,i1,i2)) by NAT_1:11;
then (mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . ((i1 -' (len (mid (f1,i1,i2)))) + 1) by A1, A2, A3, A4, A5, Th117
.= f1 . ((i1 -' ((i1 -' i2) + 1)) + 1) by A1, A2, A3, A4, A5, Th117 ;
hence (mid (f1,i1,i2)) . (len (mid (f1,i1,i2))) = f1 . i2 by A6; :: thesis: verum

end;

end;