let D be non empty set ; :: thesis: for f1 being FinSequence of D
for i1, i2, j being Element of NAT st 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 holds
(mid f1,i1,i2) . j = f1 . ((i1 -' j) + 1)
let f1 be FinSequence of D; :: thesis: for i1, i2, j being Element of NAT st 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 holds
(mid f1,i1,i2) . j = f1 . ((i1 -' j) + 1)
let i1, i2, j be Element of NAT ; :: thesis: ( 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 implies (mid f1,i1,i2) . j = f1 . ((i1 -' j) + 1) )
assume A1: ( 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 ) ; :: thesis: (mid f1,i1,i2) . j = f1 . ((i1 -' j) + 1)
then A2: j <= len (mid f1,i1,i2) by Th21;

per cases ( i1 = i2 or i2 < i1 ) by A1, XXREAL_0:1;

suppose A3: i1 = i2 ; :: thesis: (mid f1,i1,i2) . j = f1 . ((i1 -' j) + 1)

then A4: (i1 -' i2) + 1 = 0 + 1 by XREAL_1:234
.= 1 ;
then (j + i1) -' 1 = (1 + i1) -' 1 by A1, XXREAL_0:1
.= (1 + i1) - 1 by NAT_D:37
.= (i1 - 1) + 1
.= (i1 -' 1) + 1 by A1, A3, XREAL_1:235
.= (i1 -' j) + 1 by A1, A4, XXREAL_0:1 ;
hence (mid f1,i1,i2) . j = f1 . ((i1 -' j) + 1) by A1, A2, A3, JORDAN3:27; :: thesis: verum

end;

suppose A5: i2 < i1 ; :: thesis: (mid f1,i1,i2) . j = f1 . ((i1 -' j) + 1)

A6: 1 <= i1 by A1, XXREAL_0:2;
i2 <= len f1 by A1, XXREAL_0:2;
hence (mid f1,i1,i2) . j = f1 . ((i1 -' j) + 1) by A1, A2, A5, A6, JORDAN3:27; :: thesis: verum

end;

end;