let j be Nat; :: thesis: for D being non empty set
for f1 being FinSequence of D
for i1, i2 being 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 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 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 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 that
A1: 1 <= i2 and
A2: i2 <= i1 and
A3: i1 <= len f1 and
A4: 1 <= j and
A5: 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 )
A6: 1 <= i1 by A1, A2, XXREAL_0:2;
i2 - 1 >= 0 by A1, XREAL_1:48;
then A7: i1 - (i2 - 1) <= i1 - 0 by XREAL_1:10;
A8: i2 <= len f1 by A2, A3, XXREAL_0:2;
1 - j <= j - j by A4, XREAL_1:9;
then A9: (i1 -' i2) + (1 - j) <= (i1 -' i2) + 0 by XREAL_1:7;
j - j <= ((i1 -' i2) + 1) - j by A5, XREAL_1:9;
then ((i1 -' i2) + 1) -' j <= i1 -' i2 by A9, XREAL_0:def 2;
then A10: (((i1 -' i2) + 1) -' j) + 1 <= (i1 -' i2) + 1 by XREAL_1:6;
A11: 1 <= (((i1 -' i2) + 1) -' j) + 1 by NAT_1:11;
A12: (((i1 -' i2) + 1) -' j) + 1 = (((i1 -' i2) + 1) - j) + 1 by A5, XREAL_1:233
.= (((i1 - i2) + 1) - j) + 1 by A2, XREAL_1:233 ;
A13: (i1 -' i2) + 1 = (i1 - i2) + 1 by A2, XREAL_1:233;

now :: thesis: ( ( i1 > i2 & (mid (f1,i1,i2)) . j = (mid (f1,i2,i1)) . ((((i1 - i2) + 1) - j) + 1) & (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 ) or ( i1 = i2 & (mid (f1,i1,i2)) . j = (mid (f1,i2,i1)) . ((((i1 - i2) + 1) - j) + 1) & (((i1 - i2) + 1) - j) + 1 = (((i1 -' i2) + 1) -' j) + 1 ) )

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

case A14: 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, A6, A8, Th117;
then A15: (mid (f1,i2,i1)) . ((((i1 -' i2) + 1) -' j) + 1) = f1 . ((((((i1 -' i2) + 1) -' j) + 1) + i2) -' 1) by A1, A2, A3, A6, A8, A10, A11, Th117;
A16: len (mid (f1,i1,i2)) = (i1 -' i2) + 1 by A1, A3, A6, A8, A14, Th117;
(((((i1 -' i2) + 1) -' j) + 1) + i2) -' 1 = (((((i1 -' i2) + 1) -' j) + 1) + i2) - 1 by A1, NAT_D:37
.= (i1 - j) + 1 by A12
.= (i1 -' j) + 1 by A5, A13, A7, XREAL_1:233, XXREAL_0:2 ;
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, A3, A4, A5, A6, A8, A12, A14, A15, A16, Th117; :: thesis: verum

end;

case A17: 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:232
.= 1 ;
then (((i1 - i2) + 1) - j) + 1 = ((0 + 1) - 1) + 1 by A4, A5, A17, 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 A12, A17; :: 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