theorem Th16: :: FINSEQ_5:16

for f being FinSequence
for i being Nat holds len (f | i) <= len f