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 <= 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 Element of 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 Element of 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 Element of 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 A1: ( 1 <= i1 & i1 <= i2 & i2 <= len f1 & 1 <= j & 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;
A2: 1 <= (((i2 -' i1) + 1) -' j) + 1 by NAT_1:11;
j - 1 >= 0 by A1, XREAL_1:50;
then A3: ((((i2 -' i1) + 1) -' j) + 1) + 0 <= ((((i2 -' i1) + 1) -' j) + 1) + (j - 1) by XREAL_1:9;
A4: ((i2 -' i1) + 1) - j = ((i2 -' i1) + 1) -' j by A1, XREAL_1:235;
(((i2 - i1) + 1) - j) + 1 = (((i2 -' i1) + 1) - j) + 1 by A1, XREAL_1:235
.= (((i2 -' i1) + 1) -' j) + 1 by A1, XREAL_1:235 ;
then (((i2 - i1) + 1) - ((((i2 -' i1) + 1) -' j) + 1)) + 1 = j ;
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, A4, Th25; :: thesis: verum