let j be Element of NAT ; :: thesis: for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Element of NAT st 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 holds
( (mid f1,i1,i2) . j = (mid f1,i2,i1) . ((((i1 - i2) + 1) - j) + 1) & (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 )
let D be non empty set ; :: thesis: for f1 being FinSequence of D
for i1, i2 being Element of NAT st 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 holds
( (mid f1,i1,i2) . j = (mid f1,i2,i1) . ((((i1 - i2) + 1) - j) + 1) & (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 )
let f1 be FinSequence of D; :: thesis: for i1, i2 being Element of NAT st 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 holds
( (mid f1,i1,i2) . j = (mid f1,i2,i1) . ((((i1 - i2) + 1) - j) + 1) & (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 )
let i1, i2 be Element of NAT ; :: thesis: ( 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 implies ( (mid f1,i1,i2) . j = (mid f1,i2,i1) . ((((i1 - i2) + 1) - j) + 1) & (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 ) )
assume A1: ( 1 <= i2 & i2 <= i1 & i1 <= len f1 & 1 <= j & j <= (i1 -' i2) + 1 ) ; :: thesis: ( (mid f1,i1,i2) . j = (mid f1,i2,i1) . ((((i1 - i2) + 1) - j) + 1) & (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 )
then A2: 1 <= i1 by XXREAL_0:2;
A3: i2 <= len f1 by A1, XXREAL_0:2;
A4: j - j <= ((i1 -' i2) + 1) - j by A1, XREAL_1:11;
1 - j <= j - j by A1, XREAL_1:11;
then (i1 -' i2) + (1 - j) <= (i1 -' i2) + 0 by XREAL_1:9;
then ((i1 -' i2) + 1) -' j <= i1 -' i2 by A4, XREAL_0:def 2;
then A5: (((i1 -' i2) + 1) -' j) + 1 <= (i1 -' i2) + 1 by XREAL_1:8;
A6: (i1 -' i2) + 1 = (i1 - i2) + 1 by A1, XREAL_1:235;
i2 - 1 >= 0 by A1, XREAL_1:50;
then A7: i1 - (i2 - 1) <= i1 - 0 by XREAL_1:12;
A8: (((i1 -' i2) + 1) -' j) + 1 = (((i1 -' i2) + 1) - j) + 1 by A1, XREAL_1:235
.= (((i1 - i2) + 1) - j) + 1 by A1, XREAL_1:235 ;
A9: 1 <= (((i1 -' i2) + 1) -' j) + 1 by NAT_1:11;

now

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

case A10: i1 > i2 ; :: thesis: ( (mid f1,i1,i2) . j = (mid f1,i2,i1) . ((((i1 - i2) + 1) - j) + 1) & (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 )

len (mid f1,i2,i1) = (i1 -' i2) + 1 by A1, A2, A3, JORDAN3:27;
then A11: (mid f1,i2,i1) . ((((i1 -' i2) + 1) -' j) + 1) = f1 . ((((((i1 -' i2) + 1) -' j) + 1) + i2) -' 1) by A1, A2, A3, A5, A9, JORDAN3:27;
A12: (((((i1 -' i2) + 1) -' j) + 1) + i2) -' 1 = (((((i1 -' i2) + 1) -' j) + 1) + i2) - 1 by A1, NAT_D:37
.= (i1 - j) + 1 by A8
.= (i1 -' j) + 1 by A1, A6, A7, XREAL_1:235, XXREAL_0:2 ;
len (mid f1,i1,i2) = (i1 -' i2) + 1 by A1, A2, A3, A10, JORDAN3:27;
hence ( (mid f1,i1,i2) . j = (mid f1,i2,i1) . ((((i1 - i2) + 1) - j) + 1) & (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 ) by A1, A2, A3, A8, A10, A11, A12, JORDAN3:27; :: thesis: verum

end;

case A13: i1 = i2 ; :: thesis: ( (mid f1,i1,i2) . j = (mid f1,i2,i1) . ((((i1 - i2) + 1) - j) + 1) & (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 )

then (i1 -' i2) + 1 = 0 + 1 by XREAL_1:234
.= 1 ;
then (((i1 - i2) + 1) - j) + 1 = ((0 + 1) - 1) + 1 by A1, A13, XXREAL_0:1
.= 1 ;
hence ( (mid f1,i1,i2) . j = (mid f1,i2,i1) . ((((i1 - i2) + 1) - j) + 1) & (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 ) by A8, A13; :: thesis: verum

end;

end;

end;

hence ( (mid f1,i1,i2) . j = (mid f1,i2,i1) . ((((i1 - i2) + 1) - j) + 1) & (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 ) ; :: thesis: verum