theorem Th88: :: FINSEQ_1:89

for n being Nat
for f being b₁ -element FinSequence holds dom f = Seg n