theorem Th16: :: JORDAN4:16
for f1 being FinSequence holds mid (f1,0,0) = f1 | 1