theorem Th17: :: JORDAN4:17

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