theorem Th17: :: FINSEQ_6:195

for k being Nat
for f1 being FinSequence st len f1 < k holds
mid (f1,k,k) = {}