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 <= 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 Element of 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 Element of 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, Th22; :: 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:50;
then i1 - 0 >= i1 - (i2 - 1) by XREAL_1:12;
then i1 >= (i1 - i2) + 1 ;
then (i1 -' i2) + 1 <= i1 by A5, XREAL_1:235;
then A6: (i1 -' ((i1 -' i2) + 1)) + 1 = (i1 - ((i1 -' i2) + 1)) + 1 by XREAL_1:235
.= i1 - (i1 -' i2)
.= i1 - (i1 - i2) by A5, XREAL_1:235
.= i2 ;
len (mid f1,i1,i2) = (i1 -' i2) + 1 by A1, A2, A3, A4, A5, JORDAN3:27;
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, JORDAN3:27
.= f1 . ((i1 -' ((i1 -' i2) + 1)) + 1) by A1, A2, A3, A4, A5, JORDAN3:27 ;
hence (mid f1,i1,i2) . (len (mid f1,i1,i2)) = f1 . i2 by A6; :: thesis: verum

end;

end;