theorem Th16: :: FINSEQ_6:194

for f1 being FinSequence holds mid (f1,0,0) = f1 | 1