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