theorem :: FINSEQ_2:28

for i being natural Number
for D being non empty set
for q being FinSequence
for f being sequence of D st q = f | (Seg i) holds
len q = i