theorem Th58: :: FINSEQ_1:58

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