theorem Th16: :: JORDAN4:16
for D being non empty set
for f1 being FinSequence of D holds mid (f1,0,0) = f1 | 1