let j be Nat; :: thesis: for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 <= len f1 & 1 <= j & j <= (i2 -' i1) + 1 holds
( (mid (f1,i1,i2)) . j = (mid (f1,i2,i1)) . ((((i2 - i1) + 1) - j) + 1) & (((i2 - i1) + 1) - j) + 1 = (((i2 -' i1) + 1) -' j) + 1 )
let D be non empty set ; :: thesis: for f1 being FinSequence of D
for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 <= len f1 & 1 <= j & j <= (i2 -' i1) + 1 holds
( (mid (f1,i1,i2)) . j = (mid (f1,i2,i1)) . ((((i2 - i1) + 1) - j) + 1) & (((i2 - i1) + 1) - j) + 1 = (((i2 -' i1) + 1) -' j) + 1 )
let f1 be FinSequence of D; :: thesis: for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 <= len f1 & 1 <= j & j <= (i2 -' i1) + 1 holds
( (mid (f1,i1,i2)) . j = (mid (f1,i2,i1)) . ((((i2 - i1) + 1) - j) + 1) & (((i2 - i1) + 1) - j) + 1 = (((i2 -' i1) + 1) -' j) + 1 )
let i1, i2 be Nat; :: thesis: ( 1 <= i1 & i1 <= i2 & i2 <= len f1 & 1 <= j & j <= (i2 -' i1) + 1 implies ( (mid (f1,i1,i2)) . j = (mid (f1,i2,i1)) . ((((i2 - i1) + 1) - j) + 1) & (((i2 - i1) + 1) - j) + 1 = (((i2 -' i1) + 1) -' j) + 1 ) )
assume that
A1: 1 <= i1 and
A2: i1 <= i2 and
A3: i2 <= len f1 and
A4: 1 <= j and
A5: j <= (i2 -' i1) + 1 ; :: thesis: ( (mid (f1,i1,i2)) . j = (mid (f1,i2,i1)) . ((((i2 - i1) + 1) - j) + 1) & (((i2 - i1) + 1) - j) + 1 = (((i2 -' i1) + 1) -' j) + 1 )
set k = (((i2 -' i1) + 1) -' j) + 1;
(((i2 - i1) + 1) - j) + 1 = (((i2 -' i1) + 1) - j) + 1 by A2, XREAL_1:233
.= (((i2 -' i1) + 1) -' j) + 1 by A5, XREAL_1:233 ;
then A6: (((i2 - i1) + 1) - ((((i2 -' i1) + 1) -' j) + 1)) + 1 = j ;
j - 1 >= 0 by A4, XREAL_1:48;
then A7: ((((i2 -' i1) + 1) -' j) + 1) + 0 <= ((((i2 -' i1) + 1) -' j) + 1) + (j - 1) by XREAL_1:7;
A8: 1 <= (((i2 -' i1) + 1) -' j) + 1 by NAT_1:11;
((i2 -' i1) + 1) - j = ((i2 -' i1) + 1) -' j by A5, XREAL_1:233;
hence ( (mid (f1,i1,i2)) . j = (mid (f1,i2,i1)) . ((((i2 - i1) + 1) - j) + 1) & (((i2 - i1) + 1) - j) + 1 = (((i2 -' i1) + 1) -' j) + 1 ) by A1, A2, A3, A8, A7, A6, Th13; :: thesis: verum