theorem :: FINSEQ_2:27

for i being natural Number
for D being non empty set
for f being sequence of D holds f | (Seg i) is FinSequence of D