theorem :: FINSEQ_2:21

for i being natural Number
for p, q being FinSequence st q = p | (Seg i) holds
len q = min (i,(len p))