theorem Th59: :: FINSEQ_1:59

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