theorem :: FINSEQ_1:86

for n being Nat
for p, q being FinSequence st q = p | (Seg n) holds
len q <= n