theorem Th18: :: JORDAN4:18

for i1, i2 being Nat
for f1 being FinSequence holds mid (f1,i1,i2) = Rev (mid (f1,i2,i1))