theorem Th17: :: FINSEQ_5:17

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