theorem :: JORDAN4:14

for j being Nat
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 )