theorem Th88: :: FINSEQ_1:89
for n being Nat
for f being b1 -element FinSequence holds dom f = Seg n